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