proposition: Lemma rh_pres_inv : forall x:R, (f [--]x) [=] [--] (f x).
proof: Proof. intro x; apply (cg_cancel_lft S (f x)). astepr ([0]:S). astepl (f (x[+][--]x)). Step_final (f ([0]:R)); try apply rh_pres_zero. Qed.
imports: CoRN.algebra.CRings