proposition: Lemma plus_cancel_ap_rht : forall x y z : G, x[+]z [#] y[+]z -> x [#] y.
proof: Proof. Proof cg_ap_cancel_rht. Lemma minus_ap_zero : forall x y : G, x [#] y -> x [-] y [#] [0]. Proof. intros x y H. astepr (y [-] y). unfold cg_minus in |- *. apply op_rht_resp_ap; assumption. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids