Remove `frac_validI`, add `dfrac_valid`

See the discussion in !942 (diffs, comment 92602)

I am not convinced it makes sense to have internal validity lemmas (suffix I) for cmras that are always discrete such as frac, dfrac, nat, max_nat, Z, max_Z, etc. There is also just one use of frac_validI.

Relatedly, Ike noticed that dfrac_valid is missing, so I am adding that.