proposition: Lemma count_drawers : forall P Q n, n < count n P + count n Q -> { i | i < n /\ P i = true /\ Q i = true }.
proof: Proof. intros P Q n L. destruct (not_empty (inter P Q) n) as (i, Hi). rewrite count_inter. pose proof count_bound (union P Q) n. lia. exists i; intuition; unfold inter in *; destruct (P i); destruct (Q i); intuition. Defined.
imports: ZArith Lia MyNat