proposition: Lemma FunLocSorted : forall (xn : list Q), (forall n:nat, lt (S n) (length xn) -> Qle (nth n xn 0%Q) (nth (S n) xn 0%Q)) -> LocallySorted (fun x x0 : QArith_base.Q => is_true (Qle_bool x x0)) xn.
proof: Proof. induction xn. - intros. apply LSorted_nil. - intros. destruct xn. apply LSorted_cons1. apply LSorted_consn. apply IHxn. intros. apply (H (S n)). apply le_n_S, H0. unfold is_true. rewrite Qle_bool_iff. apply (H O). apply le_n_S, le_n_S, Nat.le_0_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont