proposition: Lemma incl_inv : forall x y l1 l2, Sorted lt (x::l1) -> Sorted lt (y::l2) -> incl (x::l1)(y::l2) -> y <= x /\ incl l1 l2.
proof: Proof. intros. red in H1. assert (y <= x). { specialize (H1 x (in_eq x l1)). destruct H1. subst; auto with arith. specialize (sorted_In _ _ H0 _ H1). auto with arith. } split;auto. intros z Hz. assert (x < z). { specialize (sorted_In _ _ H _ Hz). auto. } assert (y < z). eauto with arith. specialize (H1 z). destruct H1. right;auto. subst. assert (F: False) by abstract lia; elim F. auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)