proposition: Lemma cg_inv_unique' : forall x y : G, x[+]y [=] [0] -> x [=] [--] y.
proof: Proof. intros x y H. astepl (x[+][0]). astepl (x[+](y[+] [--] y)). astepl (x[+]y[+] [--] y). Step_final ([0][+] [--] y). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids