Lemma abmonoidfrac_gtmax : ∏ (x y z : abmonoidfrac X Y), (StrongOrder_abmonoidfrac Y gt Hgt) z x → (StrongOrder_abmonoidfrac Y gt Hgt) z y → (StrongOrder_abmonoidfrac Y gt Hgt) z (Lmax (abmonoidfrac_lattice X Y lat Hmin Hmax) x y). Proof. simple refine (setquotuniv3prop (eqrelabmonoidfrac X Y) (λ _ _ _, _ ,, _) _). - apply isapropimpl, isapropimpl, propproperty. - intros x y z. change (abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) z) (setquotpr (eqrelabmonoidfrac X Y) x) → abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) z) (setquotpr (eqrelabmonoidfrac X Y) y) → abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) z) (abmonoidfrac_max X Y Hmax (setquotpr (eqrelabmonoidfrac X Y) x) (setquotpr (eqrelabmonoidfrac X Y) y))). unfold abmonoidfrac_max, abmonoidfracrel, quotrel. rewrite setquotfun2comm ; do 3 rewrite setquotuniv2comm. apply hinhfun2. intros cx cy. unfold abmonoidfrac_lattice_fun. change (∑ c0 : Y, gt (pr1 z * pr1 (pr2 x * pr2 y) * pr1 c0) (Lmax lat (pr1 x * pr1 (pr2 y)) (pr1 y * pr1 (pr2 x)) * pr1 (pr2 z) * pr1 c0)). exists (@op Y (pr1 cx) (pr1 cy)). do 2 rewrite Hmax. apply Hgtmax. + change (gt (pr1 z * (pr1 (pr2 x) * pr1 (pr2 y)) * (pr1 (pr1 cx) * pr1 (pr1 cy))) (pr1 x * pr1 (pr2 y) * pr1 (pr2 z) * (pr1 (pr1 cx) * pr1 (pr1 cy)))). rewrite (assocax X (pr1 x)). rewrite (commax X (pr1 (pr2 y))). rewrite <- (assocax X (pr1 x)), <- (assocax X (pr1 z)). rewrite (assocax X (pr1 x * pr1 (pr2 z))%multmonoid), (assocax X (pr1 z * pr1 (pr2 x))%multmonoid). generalize (commax X (pr1 (pr2 y)) (pr1 (pr1 cx) * pr1 (pr1 cy))). intros ->. do 2 rewrite <- (assocax X (pr1 x * pr1 (pr2 z))%multmonoid), <- (assocax X (pr1 z * pr1 (pr2 x))%multmonoid). apply (pr2 Hgt). apply (pr2 (pr2 y)). apply (pr2 Hgt). apply (pr2 (pr1 cy)). apply (pr2 cx). + change (gt (pr1 z * (pr1 (pr2 x) * pr1 (pr2 y)) * (pr1 (pr1 cx) * pr1 (pr1 cy))) (pr1 y * pr1 (pr2 x) * pr1 (pr2 z) * (pr1 (pr1 cx) * pr1 (pr1 cy)))). rewrite (commax X (pr1 (pr1 cx))). rewrite (assocax X (pr1 y)). do 2 rewrite (commax X (pr1 (pr2 x))). rewrite <- (assocax X (pr1 y)), <- (assocax X (pr1 z)). rewrite (assocax X (pr1 y * pr1 (pr2 z))%multmonoid), (assocax X (pr1 z * pr1 (pr2 y))%multmonoid). rewrite (commax X (pr1 (pr2 x))). do 2 rewrite <- (assocax X (pr1 y * pr1 (pr2 z))%multmonoid), <- (assocax X (pr1 z * pr1 (pr2 y))%multmonoid). apply (pr2 Hgt). apply (pr2 (pr2 x)). apply (pr2 Hgt). apply (pr2 (pr1 cx)). apply (pr2 cy). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.