proposition: Lemma op_rht_resp_ap : forall x y z : G, x [#] y -> x[+]z [#] y[+]z.
proof: Proof. intros x y z H. cut (x[+]z [-] z [#] y[+]z [-] z). intros h. case (cs_bin_op_strext _ _ _ _ _ _ h). auto. intro contra; elim (ap_irreflexive _ _ contra). astepl x; astepr y. auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids