proposition: Lemma cards_eq0 A : (#|A| == 0) = (A == set0).
proof: Proof. by rewrite (eq_sym A) eqEcard sub0set cards0 leqn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)