proposition: Lemma commringfracldistr (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : isldistr (commringfracop1 X S) (commringfracop2 X S).
proof: 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'))). destruct xs as [ x s ]. destruct xs' as [ x' s' ]. destruct xs'' as [ x'' s'' ]. destruct s'' as [ s'' iss'' ]. simpl. apply hinhpr. split with (unel S). destruct s as [ s iss ]. destruct s' as [ s' iss' ]. simpl. change (paths (((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 : paths ((x'' * (s' * x)) * ((s'' * s) * (s'' * s'))) (((s'' * s') * (x'' * x)) * (s'' * (s * s')))). { destruct (assoc x'' s' x). destruct (comm s' x''). rewrite (assoc s' x'' x). destruct (comm (x'' * x) s'). destruct (comm (x'' * x) (s'' * s')). destruct (assoc s'' s s'). destruct (comm (s'' * s') (s'' * s)). destruct (comm s' (s'' * s)). destruct (rer (x'' * x) s' (s'' * s') (s'' * s)). apply idpath. } assert (e2 : paths ((x'' * (s * x')) * ((s'' * s) * (s'' * s'))) (((s'' * s) * (x'' * x')) * (s'' * (s * s')))). { destruct (assoc x'' s x'). destruct (comm s x''). rewrite (assoc s x'' x'). destruct (comm (x'' * x') s). destruct (comm (x'' * x') (s'' * s)). destruct (rer (x'' * x') (s'' * s) s (s'' * s')). destruct (assoc s s'' s'). destruct (assoc s'' s s'). destruct (comm s s''). apply idpath. } rewrite e1. rewrite e2. apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids