proposition: Lemma count_union_singleton P a n : P a = false -> a < n -> count n (union P (singleton a)) = S (count n P).
proof: Proof. intros Ma L. induction n; dumb. unfold union, singleton; simpl. destruct (eq_nat_dec a n). subst; rewrite Ma; simpl. f_equal; apply count_same_bounded; intros i Li. auto_if; dumb. rewrite plus_n_Sm, <- IHn; dumb. repeat f_equal; auto with *. Qed.
imports: ZArith Lia MyNat