proposition: Theorem check_all_occs_not_perm: forall l1 l2, check_all_occs l1 l2 l1 = false -> ~ perm l1 l2.
proof: Proof. intros l1 l2 Heq Hperm; elim (check_all_occs_false l1 l2 l1 Heq); intros n Hneq; elim Hneq; apply perm_nb_occ; assumption. Qed.
imports: List Arith