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. apply funextfun ; intros x. apply funextfun ; intros y. apply (maponpaths (λ H, abmonoidfracrel (ringmultabmonoid X) Y H x y)). apply isaprop_ispartbinophrel. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.