proposition: Lemma CSUCposPointApproxSequenceNested : forall n p : nat, x (CSUCposPointApproxSequence n) <= x (CSUCposPointApproxSequence (n + p)) /\ y (CSUCposPointApproxSequence (n+p)) <= y (CSUCposPointApproxSequence n).
proof: Proof. intros. generalize dependent n. induction p. - intros. rewrite Nat.add_0_r. destruct (CSUCposPointApproxSequence n). split; apply CRle_refl. - intro n. rewrite Nat.add_succ_r. simpl. specialize (IHp n). destruct (CSUCposPointApproxSequence n). destruct (CSUCposPointApproxStep (n + p) (CSUCposPointApproxSequence (n + p))). destruct (CSUCposPointApproxSequence (n+p)), x1. simpl. simpl in a0. split. apply (CRle_trans _ x2). apply IHp. apply a0. apply (CRle_trans _ y1). apply a0. apply IHp. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets