proposition: Lemma permut_add_cons_inside_eq : forall a a' l l1 l2, eqA a a' -> permutation l (l1 ++ l2) -> permutation (a :: l) (l1 ++ a' :: l2).
proof: Proof. intros; replace (a :: l) with ([] ++ a :: l); trivial; apply permut_add_inside_eq; trivial. Qed.
imports: Lia Relations Multiset SetoidList