fact: Definition WeavedLists {R : ConstructiveReals} (x partition : nat -> CRcarrier R) (last : nat) : Prop := forall n:nat, le n last -> (partition n <= x n /\ x n <= partition (S n)).
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont