proposition: Lemma permut_middle : forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
proof: Proof. intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl. Qed.
imports: Lia Relations Multiset SetoidList