proposition: Lemma f_pres_min : forall x y : R1, f (x[-]y)[=]f x[-]f y.
proof: Proof. intros. astepr (f (x[+][--]y)). apply f_well_def. algebra. astepr (f x[+][--](f y)). red in H3. astepr (f x[+]f [--]y). apply H3. apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply f_pres_minus. Qed.
imports: CoRN.reals.CReals