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