Lemma commringfracl2 (X : commring) (x x' x'' s s' s'' : X) : s'' * (s' * x + s * x') + (s * s') * x'' = (s' * s'') * x + s * (s'' * x' + s' * x''). 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). induction (comm2 s'' s'). induction (assoc2 s'' s' x). induction (assoc2 s'' s x'). induction (assoc2 s s'' x'). induction (comm2 s s''). induction (assoc2 s s' x''). apply (assoc1 ((s'' * s') * x) ((s * s'') * x') ((s * s') * x'')). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.