proposition: Lemma Permutation_pigeonhole l1 l2 : incl l1 l2 -> length l2 < length l1 -> exists a l3, Permutation l1 (a :: a :: l3).
proof: Proof. induction l2 as [|a l2 IH] in l1 |- *. - intros -> %incl_l_nil [] %PeanoNat.Nat.nlt_0_r. - intros [[|[|n]] [l4 [Hl1 Hl4]]] %Permutation_incl_cons_inv_r Hlen. + apply IH. * unfold incl. eauto using Permutation_in. * eauto using PeanoNat.Nat.lt_trans. + assert (Hl2l4 : length l2 < length l4). { rewrite (Permutation_length Hl1) in Hlen. now apply PeanoNat.Nat.succ_lt_mono. } destruct (IH l4 Hl4 Hl2l4) as [b [l3 Hl4l3]]. exists b, (a :: l3). apply (Permutation_trans Hl1). now apply (Permutation_cons_app (b :: b :: nil)). + now exists a, (repeat a n ++ l4). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat