proposition: Lemma permut_remove_hd : forall l l1 l2 a, permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
proof: Proof. eauto using permut_remove_hd_eq, Equivalence_Reflexive. Qed.
imports: Lia Relations Multiset SetoidList