proposition: Lemma permut_trans : forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
proof: Proof. unfold permutation; intros. apply meq_trans with (list_contents m); auto with datatypes. Qed.
imports: Lia Relations Multiset SetoidList