proposition: Theorem sorted_split_cons_not_in : ∀ l la lb a, Sorted Nat.lt l → split_list l [a … la] lb → a ∉ lb.
proof: Proof. intros l la lb a Hsort Hs Hlb. revert la lb a Hsort Hs Hlb. induction l as [| b]; intros; [ inversion Hs | idtac ]. destruct (eq_nat_dec a b) as [Hab| Hab]. subst b. inversion Hs; subst. clear Hs. eapply split_list_sorted_cons_not_in; eassumption. clear Hlb. clear Hs. apply split_list_comm in H3. eapply split_sorted_cons_r; eassumption. inversion Hs; subst. apply Hab; reflexivity. apply not_eq_sym in Hab. destruct Hlb as [| Hlb]; [ contradiction | idtac ]. eapply IHl; try eassumption. eapply Sorted_inv; eassumption. Qed.
imports: Utf8 Arith NPeano Sorted Misc