proposition: Lemma incl_decomp : forall l1 l2, Sorted lt l1 -> Sorted lt l2 -> incl l1 l2 -> exists l3 l4, l2 = l3 ++ l4 /\ ptwise_le l3 l1.
proof: Proof. induction l1. intros; exists nil, l2. split. reflexivity. constructor. destruct l2. intros. red in H1. destruct (H1 a) ;auto. now left. intros. destruct (incl_inv a n l1 l2);auto. destruct (IHl1 l2). now inversion_clear H. now inversion_clear H0. auto. destruct H4 as [l4 [H5 H6]]. subst. exists (n::x), l4. split;auto. constructor. auto. auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)