proposition: Lemma In_sorted_ge_inv : forall x y s, In x (y::s) -> sorted_ge y s -> y < x /\ In x s \/ y = x.
proof: Proof. intros x y s H H0; destruct H. - subst; auto. - destruct (lt_eq_lt_dec x y) as [[H1 | H2] | H3]. + rewrite sorted_ge_iff in H0; destruct H0. rewrite Forall_forall in H2; specialize (H2 x H). cut False; [contradiction | abstract lia ]. + subst; auto. + auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)