proposition: Lemma leq_card_setU A B : #|A :|: B| <= #|A| + #|B| ?= iff [disjoint A & B].
proof: Proof. rewrite -(addn0 #|_|) -setI_eq0 -cards_eq0 -cardsUI eq_sym. by rewrite (mono_leqif (leq_add2l _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)