proposition: Theorem f12_pres_less : fun_pres_relation R1 R2 f12 (cof_less (c:=R1)) (cof_less (c:=R2)).
proof: Proof. red in |- *. intros. unfold f12 in |- *. apply Lim_pres_less. unfold image_G_as_CauchySeq12 in |- *. change ((Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 x) m)) (inj_Q_Cauchy R2 (G_as_CauchySeq R1 x)) :R_COrdField R2)[<] Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 y) n)) (inj_Q_Cauchy R2 (G_as_CauchySeq R1 y))) in |- *. apply inj_seq_less. apply less_inj_seq with (IR := R1). change ((inj_Q_G_as_CauchySeq R1 x:R_COrdField R1)[<] (inj_Q_G_as_CauchySeq R1 y:R_COrdField R1)) in |- *. apply less_pres_Lim. apply less_wdl with (x := x). apply less_wdr with (y := y). assumption. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply SeqLimit_unique. apply x_is_SeqLimit_G. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism