proposition: Lemma less_inj_seq : forall (IR : CReals) (g h : R_COrdField Q_as_COrdField), (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) -> g[<]h.
proof: Proof. do 3 intro. intro H. simpl in |- *. red in |- *. simpl in H. red in H. simpl in H. case H. intros N H2. case H2. intros e H1 H6. set (H0 := True) in *. case (Q_dense_in_CReals IR e). assumption. intro q. set (H3 := True) in *. intros H4 H5. exists N. exists q. apply less_inj_Q with (R1 := IR). simpl in |- *. rstepl ([0]:IR). assumption. intros. apply leEq_inj_Q with (R1 := IR). apply leEq_transitive with (y := e). apply less_leEq; assumption. apply leEq_wdr with (y := inj_Q IR (CS_seq Q_as_COrdField h n)[-] inj_Q IR (CS_seq Q_as_COrdField g n)). apply H6. assumption. apply eq_symmetric_unfolded. apply inj_Q_minus. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism