proposition: Theorem check_all_occs_false: forall l1 l2 l3, check_all_occs l1 l2 l3 = false -> (exists a : A , nb_occ a l1 <> nb_occ a l2 ).
proof: Proof. simple induction l3. - simpl; intros; discriminate. - intros n l IHl; simpl. generalize (@eq_nat_bool_false (nb_occ n l1) (nb_occ n l2)). case (Nat.eqb (nb_occ n l1) (nb_occ n l2)). + auto. + intros; exists n; auto. Qed.
imports: List Arith