proposition: Lemma SeqBound0_greater : forall (m n : nat), (m < n)%nat -> AbsIR (seq m) [<=] SeqBound0 n.
proof: Proof. intros. elim H. simpl. apply lft_leEq_MAX. intros. simpl. apply leEq_transitive with (SeqBound0 m0); auto. apply rht_leEq_MAX. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq