proposition: Lemma conv_modulus : forall (x : R_COrdField') M, {N : nat | forall m, N <= m -> AbsSmall (one_div_succ M) (CS_seq F x m[-]CS_seq F x N)}.
proof: Proof. intros. case x. intros x_ px. unfold Cauchy_prop in px. cut {N : nat | forall m : nat, N <= m -> AbsSmall (one_div_succ M) (x_ m[-]x_ N)}. intro H. case H. intros N H1. exists N. intros. apply H1. assumption. apply px. apply one_div_succ_pos. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals