proposition: Lemma Permutation_middle2 : forall l1 l2 l3 a b, Permutation (a :: b :: l1 ++ l2 ++ l3) (l1 ++ a :: l2 ++ b :: l3).
proof: Proof. intros l1 l2 l3 a b. apply Permutation_cons_app. rewrite 2 app_assoc. now apply Permutation_cons_app. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat