proposition: Lemma cg_inv_inv : forall x : G, [--] [--] x [=] x.
proof: Proof. intro x. astepl ([0][+] [--] [--] x). astepl (x[+] [--] x[+] [--] [--] x). astepl (x[+]([--] x[+] [--] [--] x)). Step_final (x[+][0]). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids