proposition: Lemma ring_distr1 : forall a b1 b2:R, a [*] (b1[-]b2) [=] a[*]b1 [-] a[*]b2.
proof: Proof. intros a b1 b2. astepl (a[*](b1[+][--]b2)). astepl (a[*]b1 [+] a[*][--]b2). Step_final (a[*]b1 [+] [--](a[*]b2)). 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)