fact: Definition IntervalPartitionRefinement {R : ConstructiveReals} (a b : CRcarrier R) (small big : @IntervalPartition R a b) (subseq : nat -> nat) : Prop := (forall n:nat, le n (S (ipt_last small)) -> ipt_seq big (subseq n) == ipt_seq small n) /\ (forall n p:nat, n < p -> p <= S (ipt_last small) -> subseq n < subseq p)%nat /\ (forall n:nat, n <= S (ipt_last small) -> subseq n <= S (ipt_last big))%nat.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont