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