proposition: Lemma Permutation_app_swap_app : forall l1 l2 l3: list A, Permutation (l1 ++ l2 ++ l3) (l2 ++ l1 ++ l3).
proof: Proof. intros. rewrite 2 app_assoc. apply Permutation_app_tail, Permutation_app_comm. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat