proposition: Lemma f_pres_leEq : forall x y : R1, x[<=]y -> f x[<=]f y.
proof: Proof. intros; rewrite -> leEq_def; intro. apply less_irreflexive_unfolded with (x := x). apply leEq_less_trans with y; auto. apply less_pres_f; auto. Qed.
imports: CoRN.reals.CReals