proposition: Lemma count_image_injective : forall domain bound f, injective domain f -> bounded domain bound f -> count bound (image f domain) = domain.
proof: Proof. intros dom M f Injf Bf. induction dom. simpl; clear. induction M; auto. rewrite count_image_injective_plus_one; dumb. rewrite IHdom; dumb. apply injective_S; auto. apply bounded_S; auto. Qed.
imports: ZArith Lia MyNat