proposition: Lemma cag_ap_cancel_lft : forall x y z : G, x[+]y [#] x[+]z -> y [#] z.
proof: Proof. intros x y z H. apply ap_symmetric_unfolded. apply cg_ap_cancel_rht with x. apply ap_symmetric_unfolded. astepl (x[+]y). astepr (x[+]z). auto. Qed.
imports: CoRN.algebra.CGroups