proposition: Lemma less_pres_f : forall x y : R1, f x[<]f y -> x[<]y.
proof: Proof. intros. case (ap_imp_less R1 x y). red in H1. apply H1. apply less_imp_ap. assumption. intro. assumption. intro. exfalso. cut (f y[<]f x). change (Not (f y[<]f x)) in |- *. apply less_antisymmetric_unfolded. assumption. red in H2. apply H2. assumption. Qed.
imports: CoRN.reals.CReals