proposition: Lemma Permutation_app_inv_m l l1 l2 l3 l4 : Permutation (l1 ++ l ++ l2) (l3 ++ l ++ l4) -> Permutation (l1 ++ l2) (l3 ++ l4).
proof: Proof. intros HP. apply (Permutation_app_inv_l l). transitivity (l1 ++ l ++ l2); auto. transitivity (l3 ++ l ++ l4); auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat