proposition: Lemma setI_eq0 A B : (A :&: B == set0) = [disjoint A & B].
proof: Proof. by rewrite disjoints_subset -setD_eq0 setDE setCK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)