fact: Record IntervalPartition {R : ConstructiveReals} {a b : CRcarrier R} : Set := { ipt_seq : nat -> CRcarrier R; ipt_last : nat; ipt_head : a == ipt_seq 0; ipt_lastB : b == ipt_seq (S ipt_last); ipt_ordered : forall n:nat, le n ipt_last -> ipt_seq n <= ipt_seq (S n); }.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont