proposition: Lemma cg_add_ap_zero : forall x y : G, x[+]y [#] [0] -> x [#] [0] or y [#] [0].
proof: Proof. intros x y H. apply (cs_bin_op_strext _ csg_op x [0] y [0]). astepr ([0]:G). auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids