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