proposition: Lemma zero_minus_apart : forall x y : G, x [-] y [#] [0] -> x [#] y.
proof: Proof. unfold cg_minus in |- *. intros x y H. cut (x[+] [--] y [#] y[+] [--] y). intros h. apply (cg_ap_cancel_rht _ _ _ h). astepr ([0]:G). auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids