proposition: Lemma Permutation_app_middle : forall l l1 l2 l3 l4, Permutation (l1 ++ l2) (l3 ++ l4) -> Permutation (l1 ++ l ++ l2) (l3 ++ l ++ l4).
proof: Proof. intros l l1 l2 l3 l4 HP. now rewrite Permutation_app_swap_app, HP, Permutation_app_swap_app. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat