Lemma abmonoidfrac_notgtle : ∏ (x y : abmonoidfrac X Y), ¬ (StrongOrder_abmonoidfrac Y gt Hgt) x y → Lle (abmonoidfrac_lattice X Y lat Hmin Hmax) x y. Proof. simple refine (setquotuniv2prop (eqrelabmonoidfrac X Y) (λ _ _, _ ,, _) _). - apply isapropimpl, propproperty. - intros x y H. apply abmonoidfrac_Lle. unfold abmonoidfracrel, quotrel. rewrite setquotuniv2comm. apply hinhpr. exists (pr2 x). apply Hnotgtle. intros H0 ; apply H. change (abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) x) (setquotpr (eqrelabmonoidfrac X Y) y)). unfold abmonoidfracrel, quotrel. rewrite setquotuniv2comm. apply hinhpr. exists (pr2 x). exact H0. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.