proposition: Lemma inj_Q_one_one : forall (IR : CReals) (g h : R_COrdField Q_as_COrdField), (Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq _ g m)) (inj_Q_Cauchy IR g) :R_COrdField IR)[=] Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq _ h m)) (inj_Q_Cauchy IR h) -> g[=]h.
proof: Proof. intros. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := g) (y := h). intros. cut {N : nat | forall m : nat, N <= m -> AbsSmall (inj_Q IR e) (CS_seq IR (Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq Q_as_COrdField g m)) (inj_Q_Cauchy IR g)) m[-] CS_seq IR (Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq Q_as_COrdField h m)) (inj_Q_Cauchy IR h)) m)}. intro H1. case H1. intro N. intros. exists N. intros. cut (AbsSmall (inj_Q IR e) (CS_seq IR (Build_CauchySeq IR (fun m0 : nat => inj_Q IR (CS_seq Q_as_COrdField g m0)) (inj_Q_Cauchy IR g)) m[-] CS_seq IR (Build_CauchySeq IR (fun m0 : nat => inj_Q IR (CS_seq Q_as_COrdField h m0)) (inj_Q_Cauchy IR h)) m)). intro. cut (AbsSmall (inj_Q IR e) (inj_Q IR (CS_seq Q_as_COrdField g m[-]CS_seq Q_as_COrdField h m))). intro H5. apply AbsSmall_inj_Q with IR. auto. apply AbsSmall_wdr_unfolded with (inj_Q IR (CS_seq Q_as_COrdField g m)[-] inj_Q IR (CS_seq Q_as_COrdField h m)). assumption. apply eq_symmetric_unfolded. apply inj_Q_minus. apply a. assumption. apply Eq_alt_2_1. change (Not ((Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq Q_as_COrdField g m)) (inj_Q_Cauchy IR g) :R_COrdField IR)[#] Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq Q_as_COrdField h m)) (inj_Q_Cauchy IR h))) in |- *. apply eq_imp_not_ap. assumption. apply less_wdl with (inj_Q IR [0]). apply inj_Q_less. assumption. simpl in |- *. rational. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism