fact: Definition IntervalPartitionRational {R : ConstructiveReals} {a b : CRcarrier R} (P : @IntervalPartition R a b) : Set := { rat : list Q | (length rat = plus 2 (ipt_last P)) /\ forall n:nat, le n (S (ipt_last P)) -> ipt_seq P n == CR_of_Q R (nth n rat 0%Q) }.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont