Lemma commringfracldistr (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : isldistr (commringfracop1 X S) (commringfracop2 X S). Proof. intros. set (R := eqrelcommringfrac X S). set (mult1int := commringfracop2int X S). set (mult1 := commringfracop2 X S). set (add1int := commringfracop1int X S). set (add1 := commringfracop1 X S). unfold isldistr. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros xs xs' xs''. apply (iscompsetquotpr R (mult1int xs'' (add1int xs xs')) (add1int (mult1int xs'' xs) (mult1int xs'' xs'))). induction xs as [ x s ]. induction xs' as [ x' s' ]. induction xs'' as [ x'' s'' ]. induction s'' as [ s'' iss'' ]. simpl. apply hinhpr. exists (unel S). induction s as [ s iss ]. induction s' as [ s' iss' ]. simpl. change (((x'' * (s' * x + s * x')) * ((s'' * s) * (s'' * s'))) * 1 = (((s'' * s') * (x'' * x) + (s'' * s) * (x'' * x')) * (s'' * (s * s'))) * 1). rewrite (ringldistr X (s' * x) (s * x') x''). rewrite (ringrdistr X _ _ ((s'' * s) * (s'' * s'))). rewrite (ringrdistr X _ _ (s'' * (s * s'))). set (assoc := ringassoc2 X). set (comm := ringcomm2 X). set (rer := @abmonoidoprer X (@op2 X) (commringop2axs X)). assert (e1 : (x'' * (s' * x)) * ((s'' * s) * (s'' * s')) = ((s'' * s') * (x'' * x)) * (s'' * (s * s'))). { induction (assoc x'' s' x). induction (comm s' x''). rewrite (assoc s' x'' x). induction (comm (x'' * x) s'). induction (comm (x'' * x) (s'' * s')). induction (assoc s'' s s'). induction (comm (s'' * s') (s'' * s)). induction (comm s' (s'' * s)). induction (rer (x'' * x) s' (s'' * s') (s'' * s)). apply idpath. } assert (e2 : (x'' * (s * x')) * ((s'' * s) * (s'' * s')) = ((s'' * s) * (x'' * x')) * (s'' * (s * s'))). { induction (assoc x'' s x'). induction (comm s x''). rewrite (assoc s x'' x'). induction (comm (x'' * x') s). induction (comm (x'' * x') (s'' * s)). induction (rer (x'' * x') (s'' * s) s (s'' * s')). induction (assoc s s'' s'). induction (assoc s'' s s'). induction (comm s s''). apply idpath. } rewrite e1. rewrite e2. apply idpath. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.