proposition: Lemma PartitionMesh_ext : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (len : nat), (forall n:nat, le n len -> un n == vn n) -> PartitionMesh un len == PartitionMesh vn len.
proof: Proof. induction len. - intros. reflexivity. - intros. simpl. rewrite IHlen. rewrite (H (S len)), (H len). reflexivity. apply le_S, Nat.le_refl. apply Nat.le_refl. intros. apply H. apply le_S, H0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont