proposition: Lemma Permutation_pigeonhole_rel (R : B -> A -> Prop) (l1 : list B) l2 : Forall (fun b => Exists (R b) l2) l1 -> length l2 < length l1 -> exists b b' (l3 : list B), Permutation l1 (b :: b' :: l3) /\ exists a, In a l2 /\ R b a /\ R b' a.
proof: Proof. intros [l2' [Hl2'l1 Hl2'l2]]%Forall_Exists_exists_Forall2. intros Hl2l2'. rewrite (Forall2_length Hl2'l1) in Hl2l2'. destruct (Permutation_pigeonhole Hl2'l2 Hl2l2') as [a [l3 Hl2']]. destruct (Permutation_Forall2 Hl2' (Forall2_flip Hl2'l1)) as [l1' [Hl1l1' Hl1']]. destruct (Forall2_app_inv_l [a; a] l3 Hl1') as [lbb' [l1'' [Ha [? ?]]]]. assert (Hlbb' := Forall2_length Ha). destruct lbb' as [|b lb']; [easy|]. apply Forall2_cons_iff in Ha as [Hba Ha]. destruct lb' as [|b' l]; [easy|]. apply Forall2_cons_iff in Ha as [Hb'a Ha]. inversion Ha. subst. exists b, b', l1''. split; [easy|]. exists a. split; eauto using Permutation_in, in_eq. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat