proposition: Theorem sorted_split_in_not_in : ∀ l la lb x, Sorted Nat.lt l → split_list l la lb → x ∈ la → x ∉ lb.
proof: Proof. intros l la lb x Hsort Hs Hla Hlb. revert la lb x Hsort Hs Hla Hlb. induction l as [| a]; intros. inversion Hs; subst; contradiction. rename a into y. destruct la as [| a]; [ contradiction | idtac ]. destruct Hla as [Hla| Hla]. subst x. destruct (eq_nat_dec y a) as [Hya| Hya]. subst y. inversion Hs; subst. revert Hlb. eapply split_list_sorted_cons_not_in; eassumption. rename l₂ into lb. eapply split_list_comm in H3. clear Hs. eapply split_sorted_cons_r; eassumption. destruct lb as [| b]; [ contradiction | idtac ]. destruct Hlb as [Hlb| Hlb]. subst b. inversion Hs; subst. apply Hya; reflexivity. apply Hya; reflexivity. destruct (eq_nat_dec y b) as [Hyb| Hyb]. subst y. inversion Hs; subst. apply Hya; reflexivity. clear Hs. apply Sorted_inv_1 in Hsort. eapply sorted_split_cons_not_in; eassumption. inversion Hs; subst. apply Hya; reflexivity. apply Hyb; reflexivity. destruct (eq_nat_dec y a) as [Hya| Hya]. subst y. inversion Hs; subst. apply Sorted_inv_1 in Hsort. eapply IHl; eassumption. rename l₂ into lb. eapply split_list_comm in H3. clear Hs. eapply split_sorted_cons_r; eassumption. destruct lb as [| b]; [ contradiction | idtac ]. destruct Hlb as [Hlb| Hlb]. subst b. inversion Hs; subst. apply Hya; reflexivity. clear Hs. apply split_list_comm in H2. revert Hla. eapply split_list_sorted_cons_cons; eassumption. destruct (eq_nat_dec y b) as [Hyb| Hyb]. subst y. inversion Hs; subst. apply Hya; reflexivity. clear Hs. apply Sorted_inv_1 in Hsort. eapply IHl; try eassumption. right; assumption. inversion Hs; subst. apply Hya; reflexivity. apply Hyb; reflexivity. Qed.
imports: Utf8 Arith NPeano Sorted Misc