proposition: Lemma LocSortedFun : forall (xn : list Q), LocallySorted (fun x x0 : QArith_base.Q => is_true (Qle_bool x x0)) xn -> (forall n:nat, lt (S n) (length xn) -> Qle (nth n xn 0%Q) (nth (S n) xn 0%Q)).
proof: Proof. induction xn. - intros. exfalso; inversion H0. - intros. simpl in H0. destruct xn. exfalso; inversion H0; inversion H2. destruct n. simpl. inversion H. unfold is_true in H5. rewrite Qle_bool_iff in H5. exact H5. apply IHxn. inversion H; exact H3. apply le_S_n in H0. exact H0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont