proposition: Theorem g21_strong_ext : fun_strext g21.
proof: Proof. intros. red in |- *. unfold g21 in |- *. intros x y H. case (ap_imp_less R1 (Lim (image_G_as_CauchySeq21 x)) (Lim (image_G_as_CauchySeq21 y)) H). intro. apply less_imp_ap. apply less_wdl with (x := Lim (inj_Q_G_as_CauchySeq R2 x)). apply less_wdr with (y := Lim (inj_Q_G_as_CauchySeq R2 y)). apply Lim_pres_less. unfold inj_Q_G_as_CauchySeq in |- *. change ((Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 x) m)) (inj_Q_Cauchy R2 (G_as_CauchySeq R2 x)) :R_COrdField R2)[<] Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 y) n)) (inj_Q_Cauchy R2 (G_as_CauchySeq R2 y))) in |- *. apply inj_seq_less. apply less_inj_seq with (IR := R1). change ((image_G_as_CauchySeq21 x:R_COrdField R1)[<] (image_G_as_CauchySeq21 y:R_COrdField R1)) in |- *. apply less_pres_Lim. assumption. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. intro. apply Greater_imp_ap. apply less_wdl with (x := Lim (inj_Q_G_as_CauchySeq R2 y)). apply less_wdr with (y := Lim (inj_Q_G_as_CauchySeq R2 x)). apply Lim_pres_less. unfold inj_Q_G_as_CauchySeq in |- *. change ((Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 y) m)) (inj_Q_Cauchy R2 (G_as_CauchySeq R2 y)) :R_COrdField R2)[<] Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 x) n)) (inj_Q_Cauchy R2 (G_as_CauchySeq R2 x))) in |- *. apply inj_seq_less. apply less_inj_seq with (IR := R1). change ((image_G_as_CauchySeq21 y:R_COrdField R1)[<] (image_G_as_CauchySeq21 x:R_COrdField R1)) in |- *. apply less_pres_Lim. assumption. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism