proposition: Lemma SubSeqCvMerge : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (sub : nat -> nat) (l : CRcarrier R), (forall n:nat, le n (sub n)) -> CR_cv R un l -> CR_cv R (fun n => un (sub n)) l.
proof: Proof. intros. intros n. specialize (H0 n) as [p pmaj]. exists p. intros. apply pmaj. apply (Nat.le_trans _ i _ H0), H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal