proposition: Lemma isringaddcommringfracgt (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) : @isbinophrel (commringfrac X S) (commringfracgt X S is0 is1 is2).
proof: Proof. intros. set (rer2 := (abmonoidrer (ringmultabmonoid X)) : ∏ a b c d : X, paths ((a * b) * (c * d)) ((a * c) * (b * d))). apply isbinophrelif. intros a b. apply (ringcomm1 (commringfrac X S) a b). assert (int : ∏ (a b c : ringaddabgr (commringfrac X S)), isaprop (commringfracgt X S is0 is1 is2 a b -> commringfracgt X S is0 is1 is2 (op c a) (op c b))). { intros a b c. 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 xa1 xa2 -> abmonoidfracrelint (ringmultabmonoid X) S R (commringfracop1int X S xa3 xa1) (commringfracop1int X S xa3 xa2)). simpl. apply hinhfun. intro t2. set (c0s := pr1 t2). set (c0 := pr1 c0s). set (r := pr2 t2). split with c0s. 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)). change (pr1 (R ((a1 * x3 + a3 * x1) * (a3 * a2) * c0) ((a2 * x3 + a3 * x2) * (a3 * a1) * c0))). rewrite (ringassoc2 X _ _ c0). rewrite (ringassoc2 X _ (a3 * _) c0). rewrite (ringrdistr X _ _ _). rewrite (ringrdistr X _ _ _). rewrite (rer2 _ x3 _ _). rewrite (rer2 _ x3 _ _). rewrite (ringcomm2 X a3 a2). rewrite (ringcomm2 X a3 a1). rewrite (pathsinv0 (ringassoc2 X a1 a2 a3)). rewrite (pathsinv0 (ringassoc2 X a2 a1 a3)). rewrite (ringcomm2 X a1 a2). apply ((pr1 is0) _ _ _). rewrite (ringcomm2 X a2 a3). rewrite (ringcomm2 X a1 a3). rewrite (ringassoc2 X a3 a2 c0). rewrite (ringassoc2 X a3 a1 c0). rewrite (rer2 _ x1 a3 _). rewrite (rer2 _ x2 a3 _). rewrite (pathsinv0 (ringassoc2 X x1 _ _)). rewrite (pathsinv0 (ringassoc2 X x2 _ _)). apply ((isringmultgttoislringmultgt X is0 is1) _ _ _ (is2 _ (pr2 (@op S (pr2 xa3) (pr2 xa3)))) r). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids