proposition: Lemma WeavedListSelf : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (last : nat), (forall n:nat, le n last -> (xn n) <= (xn (S n))) -> WeavedLists xn xn last.
proof: Proof. intros R xn last H n H0. split. apply CRle_refl. apply H. exact H0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont