proposition: Lemma cg_ap_cancel_rht : forall x y z : G, x[+]z [#] y[+]z -> x [#] y.
proof: Proof. intros x y z H. apply ap_wdr_unfolded with (y[+]z [-] z). apply ap_wdl_unfolded with (x[+]z [-] z). apply (op_rht_resp_ap _ _ [--] z H). astepr (x[+][0]). Step_final (x[+](z [-] z)). astepr (y[+][0]). Step_final (y[+](z [-] z)). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids