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