proposition: Theorem split_sorted_cons_r : ∀ l la lb b, split_list l la [b … lb] → Sorted Nat.lt [b … l] → False.
proof: Proof. intros l la lb b Hs Hsort. revert b lb l Hs Hsort. induction la as [| a]; intros. inversion Hs; subst. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. revert Hrel; apply Nat.lt_irrefl. destruct l as [| c]; inversion Hs; subst. eapply IHla; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. revert Hrel; apply Nat.lt_irrefl. Qed.
imports: Utf8 Arith NPeano Sorted Misc