proposition: Lemma minus_resp_ap_rht : forall x y z : G, x [#] y -> x [-] z [#] y [-] z.
proof: Proof. intros x y z H. unfold cg_minus in |- *. apply op_rht_resp_ap. assumption. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids