proposition: Lemma StrongOrder_correct_commrngfrac (X : commring) (Y : @subabmonoid (ringmultabmonoid X)) (gt : StrongOrder X) Hgt Hle Hmult Hpos : commringfracgt X Y (R := gt) Hle Hmult Hpos = StrongOrder_abmonoidfrac Y gt Hgt.
proof: Proof. apply funextfun ; intros x. apply funextfun ; intros y. apply (maponpaths (λ H, abmonoidfracrel (ringmultabmonoid X) Y H x y)). apply isaprop_ispartbinophrel. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids