proposition: Lemma inj_seq_less : forall (IR : CReals) (g h : R_COrdField Q_as_COrdField), g[<]h -> (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).
proof: Proof. do 3 intro. intro H. simpl in |- *. red in |- *. simpl in H. red in H. case H. intros N H2. case H2. intros e H1 H3. set (H0 := True) in *. exists N. exists (inj_Q IR e). apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. assumption. simpl in |- *. rational. intros. simpl in |- *. apply leEq_wdr with (y := inj_Q IR (CS_seq Q_as_COrdField h n[-]CS_seq Q_as_COrdField g n)). apply inj_Q_leEq. apply H3. assumption. apply inj_Q_minus. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism