proposition: Lemma inv_resp_ap_zero : forall x : G, x [#] [0] -> [--] x [#] [0].
proof: Proof. intros x H. astepl ([0][+] [--] x). astepl ([0] [-] x). apply minus_ap_zero. apply (ap_symmetric G). auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CMonoids