proposition: Lemma minus_cancel_ap_rht : forall x y z : G, x [-] z [#] y [-] z -> x [#] y.
proof: Proof. unfold cg_minus in |- *. intros x y z H. exact (plus_cancel_ap_rht _ _ _ H). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids