proposition: Lemma f_pres_minus : forall x : R1, f [--]x[=][--](f x).
proof: Proof. intro. apply cg_cancel_lft with (x := f x). astepr ([0]:R2). astepl (f (x[+][--]x)). astepr (f [0]). apply f_well_def. algebra. apply f_pres_One. Qed.
imports: CoRN.reals.CReals