proposition: Lemma LastNth : forall (xn : list Q), lt 0 (length xn) -> last xn 0%Q = nth (pred (length xn)) xn 0%Q.
proof: Proof. induction xn. - reflexivity. - intros. clear H. destruct xn. reflexivity. transitivity (last (q :: xn) 0%Q). reflexivity. rewrite IHxn. reflexivity. simpl. apply le_n_S, Nat.le_0_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont