proposition: Lemma count_image_injective_plus_one : forall domain f bound, injective (S domain) f -> bounded (S domain) bound f -> count bound (image f (S domain)) = S (count bound (image f domain)).
proof: Proof. intros dom f M If Bf. pose proof image_injective_plus_one dom f as HS. erewrite count_same; [ | eassumption ]. rewrite count_union_singleton; dumb. apply image_false_pr; intros i L E. apply If in E; dumb. Qed.
imports: ZArith Lia MyNat