proposition: Lemma mult_assoc_unfolded : forall x y z : R, x[*] (y[*]z) [=] x[*]y[*]z.
proof: Proof. Proof mult_assoc R. Lemma mult_commut_unfolded : forall x y : R, x[*]y [=] y[*]x. Proof mult_commutes R. Hint Resolve mult_commut_unfolded: algebra. Lemma mult_one : forall x : R, x[*][1] [=] x. Proof cm_rht_unit mmR. Lemma one_mult : forall x : R, [1][*]x [=] x. Proof cm_lft_unit mmR. Lemma ring_dist_unfolded : forall x y z : R, x[*] (y[+]z) [=] x[*]y[+]x[*]z. Proof dist R. Hint Resolve ring_dist_unfolded: algebra. Lemma ring_distl_unfolded : forall x y z : R, (y[+]z) [*]x [=] y[*]x[+]z[*]x. Proof. intros x y z. astepl (x[*] (y[+]z)). astepl (x[*]y[+]x[*]z). astepl (y[*]x[+]x[*]z). Step_final (y[*]x[+]z[*]x). 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)