proposition: Lemma sorted_max_1 : forall s n, sorted_ge n s -> (n <= simple_last n s)%nat.
proof: Proof. induction s; cbn. - auto with arith. - intros; destruct s. + now inversion_clear H. + inversion_clear H; transitivity a; auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)