proposition: Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
proof: Proof. intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l'). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat