proposition: Lemma inj_seq_well_def : forall (IR : CReals) (g h : R_COrdField Q_as_COrdField), g[=]h -> (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).
proof: Proof. intros. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq _ g m)) (inj_Q_Cauchy IR g)) (y := Build_CauchySeq IR (fun m : nat => inj_Q IR (CS_seq Q_as_COrdField h m)) (inj_Q_Cauchy IR h)). intros. simpl in |- *. case (Q_dense_in_CReals IR (e [/]TwoNZ)). apply pos_div_two. assumption. intro q. set (H1 := True) in *. intros H2 H3. cut {N : nat | forall m : nat, N <= m -> AbsSmall q (CS_seq Q_as_COrdField g m[-]CS_seq Q_as_COrdField h m)}. intro H4. case H4. intro N. intro H5. exists N. intros. apply AbsSmall_wdr_unfolded with (y := inj_Q IR (CS_seq Q_as_COrdField g m[-]CS_seq Q_as_COrdField h m)). apply AbsSmall_leEq_trans with (inj_Q IR q). apply less_leEq; apply less_transitive_unfolded with (e [/]TwoNZ). assumption. apply pos_div_two'; auto. apply inj_Q_AbsSmall. apply H5. assumption. apply inj_Q_minus. apply Eq_alt_2_1. change (Not (g[#]h)) in |- *. apply eq_imp_not_ap. assumption. apply less_inj_Q with (R1 := IR). apply less_wdl with ([0]:IR). assumption. simpl in |- *. rational. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism