proposition: Lemma commringfracl2 (X : commring) (x x' x'' s s' s'' : X) : paths ((s'' * ((s' * x) + (s * x'))) + ((s * s') * x'')) (((s' * s'') * x) + (s * ((s'' * x') + (s' * x'')))).
proof: Proof. intros. set (ldistr := ringldistr X). set (comm2 := ringcomm2 X). set (assoc2 := ringassoc2 X). set (assoc1 := ringassoc1 X). rewrite (ldistr (s' * x) (s * x') s''). rewrite (ldistr (s'' * x') (s' * x'') s). destruct (comm2 s'' s'). destruct (assoc2 s'' s' x). destruct (assoc2 s'' s x'). destruct (assoc2 s s'' x'). destruct (comm2 s s''). destruct (assoc2 s s' x''). apply (assoc1 ((s'' * s') * x) ((s * s'') * x') ((s * s') * x'')). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids