proposition: Lemma modulus_property : forall x M m0 m1, T x M <= m0 -> T x M <= m1 -> AbsSmall (Two[*]one_div_succ M) (CS_seq F x m0[-]CS_seq F x m1).
proof: Proof. intros. rstepl (one_div_succ (R:=F) M[+]one_div_succ M). rstepr (CS_seq F x m0[-]CS_seq F x (T x M) [+] (CS_seq F x (T x M) [-]CS_seq F x m1)). generalize (PT x M). intro. apply AbsSmall_plus. apply H1. assumption. apply AbsSmall_minus. apply H1. assumption. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals