proposition: Lemma ring_distr2 : forall a1 a2 b:R, (a1[-]a2) [*] b [=] a1[*]b [-] a2[*]b.
proof: Proof. intros a1 a2 b. astepl ((a1[+][--]a2)[*]b). astepl (a1[*]b [+] [--]a2[*]b). Step_final (a1[*]b [+] [--](a2[*]b)). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)