proposition: Lemma LastCons : forall (xn : list Q) (q : Q), lt 0 (length xn) -> last (q :: xn) 0%Q = last xn 0%Q.
proof: Proof. intros. destruct xn. exfalso; inversion H. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont