Lemma abmonoidfrac_lenotgt : ∏ (x y : abmonoidfrac X Y), Lle (abmonoidfrac_lattice X Y lat Hmin Hmax) x y → ¬ (StrongOrder_abmonoidfrac Y gt Hgt) x y. Proof. simple refine (setquotuniv2prop (eqrelabmonoidfrac X Y) (λ _ _, _ ,, _) _). + apply isapropimpl, isapropimpl, isapropempty. + intros x y H. apply (pr2 (abmonoidfrac_Lle _ _ _ _ _ _ _)) in H. change (abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) x) (setquotpr (eqrelabmonoidfrac X Y) y) → ∅). revert H. unfold abmonoidfracrel, quotrel. do 2 rewrite setquotuniv2comm. apply (hinhuniv2 (P := make_hProp _ isapropempty)). intros c c'. refine (Hlenotgt _ _ _ _). 2: apply (pr2 c'). unfold Lle. rewrite <- Hmin. apply (maponpaths (λ x, op x _)). apply (Hop (pr1 c)). rewrite Hmin. apply (pr2 c). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.