proposition: Lemma expand_Q_R_2 : forall x e N, [0] [<] e -> (forall m, N <= m -> AbsSmall (e [/]FourNZ) (CS_seq F x m[-]CS_seq F x N)) -> AbsSmall (inject_Q e) (inject_Q (CS_seq F x N) [-]x).
proof: Proof. intros x e N H H0. apply expand_Q_R with (x := x) (e := e) (N := N). assumption. intros. apply H0. assumption. constructor. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals