proposition: Lemma Fun2ListLength : forall (xn : nat -> Q) (len : nat), length (Fun2List xn len) = len.
proof: Proof. induction len. - reflexivity. - simpl. rewrite app_length, IHlen, Nat.add_comm. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont