proposition: Lemma ControlSubSeqCvInc : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l : CRcarrier R) (bound : nat -> CRcarrier R) (cv : CR_cv _ un l) (boundPos : forall k:nat, 0 < bound k) (n : nat), lt (let (k,_) := ControlSubSeqCv un l bound cv boundPos n in k) (let (k,_) := ControlSubSeqCv un l bound cv boundPos (S n) in k).
proof: Proof. intros. simpl. destruct (Un_cv_nat_real un l cv (bound (S n)) (boundPos (S n))), (ControlSubSeqCv un l bound cv boundPos n). apply (Nat.lt_le_trans _ (S x0)). apply le_n_S, Nat.le_refl. apply Nat.le_max_r. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions