proposition: Lemma tuto_cardUI : forall A B, #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B|.
proof: Proof. by move=> A B; rewrite !cardE /= !size_filter count_predUI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)