proposition: Lemma rh_apzero : forall x:R, (f x) [#] [0] -> x [#] [0].
proof: Proof. intros x X; apply (cg_ap_cancel_rht R x ([0]:R) x). astepr x. apply (rh_strext f (x[+]x) x). astepl ((f x)[+](f x)). astepr (([0]:S) [+] (f x)). apply (op_rht_resp_ap S (f x) ([0]:S) (f x)). assumption. Qed.
imports: CoRN.algebra.CRings