proposition: Theorem split_list_sorted_cons_not_in : ∀ l la lb a, split_list l la lb → Sorted Nat.lt [a … l] → a ∉ lb.
proof: Proof. intros l la lb a Hs Hsort Hlb. destruct lb as [| b]; intros; [ contradiction | idtac ]. destruct Hlb as [Hlb| Hlb]. subst a. eapply split_sorted_cons_r; eassumption. eapply split_list_sorted_cons_cons; eassumption. Qed.
imports: Utf8 Arith NPeano Sorted Misc