Lemma isringmultcommringfracgt (X : commring) (S : @submonoid (ringmultabmonoid X)) {R : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) R) (is1 : isringmultgt X R) (is2 : ∏ c : X, S c → R c 0) : isringmultgt (commringfrac X S) (commringfracgt X S is0 is1 is2). Proof. intros. set (rer2 := abmonoidrer (ringmultabmonoid X) : ∏ a b c d : X, (a * b) * (c * d) = (a * c) * (b * d)). apply islringmultgttoisringmultgt. assert (int : ∏ (a b c : ringaddabgr (commringfrac X S)), isaprop (commringfracgt X S is0 is1 is2 c 0 → commringfracgt X S is0 is1 is2 a b → commringfracgt X S is0 is1 is2 (c * a) (c * b))). { intros a b c. apply impred. intro. apply impred. intro. apply (pr2 _). } apply (setquotuniv3prop _ (λ a b c, make_hProp _ (int a b c))). intros xa1 xa2 xa3. change (abmonoidfracrelint (ringmultabmonoid X) S R xa3 (0 ,, unel S) → abmonoidfracrelint (ringmultabmonoid X) S R xa1 xa2 → abmonoidfracrelint (ringmultabmonoid X) S R (commringfracop2int X S xa3 xa1) (commringfracop2int X S xa3 xa2)). simpl. apply hinhfun2. intros t21 t22. set (c1s := pr1 t21). set (c1 := pr1 c1s). set (r1 := pr2 t21). set (c2s := pr1 t22). set (c2 := pr1 c2s). set (r2 := pr2 t22). set (x1 := pr1 xa1). set (a1 := pr1 (pr2 xa1)). set (x2 := pr1 xa2). set (a2 := pr1 (pr2 xa2)). set (x3 := pr1 xa3). set (a3 := pr1 (pr2 xa3)). exists (@op S c1s c2s). change (pr1 (R (x3 * x1 * (a3 * a2) * (c1 * c2)) (x3 * x2 * (a3 * a1) * (c1 * c2)))). rewrite (ringcomm2 X a3 a2). rewrite (ringcomm2 X a3 a1). rewrite (ringassoc2 X _ _ (c1 * c2)). rewrite (ringassoc2 X (x3 * x2) _ (c1 * c2)). rewrite (rer2 _ a3 c1 _). rewrite (rer2 _ a3 c1 _). rewrite (ringcomm2 X a2 c1). rewrite (ringcomm2 X a1 c1). rewrite <- (ringassoc2 X (x3 * x1) _ _). rewrite <- (ringassoc2 X (x3 * x2) _ _). rewrite (rer2 _ x1 c1 _). rewrite (rer2 _ x2 c1 _). rewrite (ringcomm2 X a3 c2). rewrite <- (ringassoc2 X _ c2 a3). rewrite <- (ringassoc2 X _ c2 _). apply ((isringmultgttoisrringmultgt X is0 is1) _ _ _ (is2 _ (pr2 (pr2 xa3)))). rewrite (ringassoc2 X _ _ c2). rewrite (ringassoc2 X _ (x2 * a1) c2). simpl in r1. clearbody r1. simpl in r2. clearbody r2. change (pr1 (R (x3 * 1 * c1) (0 * a3 * c1))) in r1. rewrite (ringrunax2 _ _) in r1. rewrite (ringmult0x X _) in r1. rewrite (ringmult0x X _) in r1. apply ((isringmultgttoislringmultgt X is0 is1) _ _ _ r1 r2). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.