proposition: Lemma sorted_ge_iff0 : forall l n, sorted_ge n l <-> LocallySorted Peano.lt l /\ List.Forall (fun i => n <= i) l.
proof: Proof. induction l. - split; auto with lists. split; auto with lists; constructor. - destruct l. + split. * split; auto with lists. constructor. constructor. eapply sorted_head; eauto. constructor. * destruct 1; constructor; inversion H0;auto. + repeat split. * inversion_clear H; auto. rewrite IHl in H2. constructor;tauto. * inversion_clear H. rewrite IHl in H2. constructor; auto. destruct H2. eapply Forall_impl. 2:eapply H2. intros; transitivity a. auto. apply H3. * destruct 1. constructor. inversion_clear H0; auto. inversion_clear H; auto. inversion_clear H. rewrite IHl. split; auto. constructor; auto with arith. apply Sorted_extends. intros x y z Hxy Hyz. eauto with arith. apply Sorted_mono with Peano.lt. eauto with arith. rewrite <- Sorted_LocallySorted_iff in H1. inversion_clear H1. constructor;auto. induction H3. constructor. constructor. eauto with arith. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)