proposition: Lemma mult_minus1 : forall x:R, [--][1] [*] x [=] [--]x.
proof: Proof. intro x. apply (cg_cancel_lft R x). astepr ([0]:R). astepl (([1][*]x)[+]([--][1][*]x)). astepl (([1][+][--][1])[*]x). Step_final ([0][*]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)