proposition: Lemma Permutation_vs_cons_cons_inv : forall l l' a b, Permutation l (a :: b :: l') -> exists l1 l2 l3, l = l1 ++ a :: l2 ++ b :: l3 \/ l = l1 ++ b :: l2 ++ a :: l3.
proof: Proof. intros l l' a b HP. destruct (Permutation_vs_cons_inv HP) as [l1 [l2]]; subst. symmetry in HP. apply Permutation_cons_app_inv in HP. apply (Permutation_in b), in_app_or in HP; [|now apply in_eq]. destruct HP as [(l3 & l4 & ->)%in_split | (l3 & l4 & ->)%in_split]. - exists l3, l4, l2; right. now rewrite <-app_assoc; simpl. - now exists l1, l3, l4; left. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat