proposition: Lemma cg_inverse : forall x : G, is_inverse csg_op [0] x [--] x.
proof: Proof. Proof cg_proof G. End CGroup_axioms. Section CGroup_basics. Variable G : CGroup. Lemma cg_rht_inv_unfolded : forall x : G, x[+] [--] x [=] [0]. Proof. intro x; elim (cg_inverse G x); auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids