proposition: Lemma cardUI A B : #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B|.
proof: Proof. by rewrite !cardE !size_filter count_predUI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)