proposition: Lemma modulus_property_2 : forall x M m, T x M <= m -> AbsSmall (one_div_succ M) (CS_seq F x m[-]CS_seq F x (T x M)).
proof: Proof. intros. apply (PT x M). assumption. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals