proposition: Lemma count_union_inter n P Q : (count n (union P Q) + count n (inter P Q) = count n P + count n Q)%nat.
proof: Proof. induction n; auto; simpl. unfold IBN, union, inter in *. remember (P n) as Pn; remember (Q n) as Qn. destruct Pn; destruct Qn; simpl; lia. Qed.
imports: ZArith Lia MyNat