fact: Definition F_ind3@{i j} (P : F -> F -> F -> Type@{i}) {sP : forall x y z, IsHProp (P x y z)} (dclass : forall x y z : Frac R, P (' x) (' y) (' z)) : forall x y z, P x y z.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields