proposition: Lemma PartitionMesh_nonneg : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (n : nat), 0 <= PartitionMesh xn n.
proof: Proof. induction n. apply CRle_refl. simpl. apply (CRle_trans _ _ _ IHn), CRmax_r. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont