proposition: Lemma permut_sym_app : forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
proof: Proof. intros l1 l2; unfold permutation, meq; intro a; do 2 rewrite list_contents_app; simpl; auto with arith. Qed.
imports: Lia Relations Multiset SetoidList