proposition: Lemma sorted_max_2 : forall s n, sorted_ge n s -> Forall (fun i => (i <= simple_last n s)%nat) s.
proof: Proof. induction s; cbn. - intros; simpl; constructor. - constructor. + apply sorted_max_1; inversion H;auto with lists. + apply IHs; eapply sorted_tail'; eauto with lists. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)