proposition: Lemma abmonoidfrac_gtmin : ∏ (x y z : abmonoidfrac X Y), (StrongOrder_abmonoidfrac Y gt Hgt) x z → (StrongOrder_abmonoidfrac Y gt Hgt) y z → (StrongOrder_abmonoidfrac Y gt Hgt) (Lmin (abmonoidfrac_lattice X Y lat Hmin Hmax) x y) z.
proof: Proof. simple refine (setquotuniv3prop (eqrelabmonoidfrac X Y) (λ _ _ _, _ ,, _) _). - apply isapropimpl, isapropimpl, propproperty. - intros x y z. change (abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) x) (setquotpr (eqrelabmonoidfrac X Y) z) → abmonoidfracrel X Y Hgt (setquotpr (eqrelabmonoidfrac X Y) y) (setquotpr (eqrelabmonoidfrac X Y) z) → abmonoidfracrel X Y Hgt (abmonoidfrac_min X Y Hmin (setquotpr (eqrelabmonoidfrac X Y) x) (setquotpr (eqrelabmonoidfrac X Y) y)) (setquotpr (eqrelabmonoidfrac X Y) z)). unfold abmonoidfrac_min, abmonoidfracrel, quotrel. rewrite setquotfun2comm ; do 3 rewrite setquotuniv2comm. apply hinhfun2. intros cx cy. unfold abmonoidfrac_lattice_fun. simpl. exists (@op Y (pr1 cx) (pr1 cy)). do 2 rewrite Hmin. apply Hgtmin. + change (gt (pr1 x * pr1 (pr2 y) * pr1 (pr2 z) * (pr1 (pr1 cx) * pr1 (pr1 cy))) (pr1 z * (pr1 (pr2 x) * pr1 (pr2 y)) * (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 y * pr1 (pr2 x) * pr1 (pr2 z) * (pr1 (pr1 cx) * pr1 (pr1 cy))) (pr1 z * (pr1 (pr2 x) * pr1 (pr2 y)) * (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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups