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