proposition: Theorem split_list_sorted_cons_cons : ∀ l la lb a b, split_list l la [b … lb] → Sorted Nat.lt [a … l] → a ∉ lb.
proof: Proof. intros l la lb a b Hs Hsort Hlb. revert la lb a b Hs Hsort Hlb. induction l as [| c]; intros; [ inversion Hs | idtac ]. destruct (eq_nat_dec c b) as [Hcb| Hcb]. subst c. inversion Hs; subst. eapply IHl; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. clear Hs. destruct lb as [| c]; [ contradiction | idtac ]. destruct Hlb as [Hlb| Hlb]. subst c. eapply split_sorted_cons_r; [ eassumption | idtac ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. eapply IHl; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. inversion Hs; subst. clear Hs. eapply IHl; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. apply Hcb; reflexivity. Qed.
imports: Utf8 Arith NPeano Sorted Misc