proposition: Lemma Fun2ListNth : forall (xn : nat -> Q) (len n : nat), lt n len -> nth n (Fun2List xn len) 0%Q = xn n.
proof: Proof. induction len. - intros. exfalso; inversion H. - intros. simpl. apply Nat.le_succ_r in H. destruct H. rewrite app_nth1. apply IHlen. exact H. rewrite Fun2ListLength. exact H. inversion H. rewrite app_nth2. rewrite Fun2ListLength, Nat.sub_diag. reflexivity. rewrite Fun2ListLength. apply Nat.le_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont