proposition: Lemma permut_length : forall l1 l2, permutation l1 l2 -> length l1 = length l2.
proof: Proof. induction l1; intros l2 H. - rewrite (permut_nil (permut_sym H)); auto. - destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)). subst l2. rewrite app_length. simpl; rewrite <- plus_n_Sm; f_equal. rewrite <- app_length. apply IHl1. apply permut_remove_hd with a; auto with typeclass_instances. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation