proposition: Lemma card_nonempty x: cardinal x = \0c -> x = emptyset.
proof: Proof. rewrite - cardinal_set0; move /card_eqP => [y [[[fy _] suy] sy ty]]. apply /set0_P => z zx; empty_tac1 (Vf y z); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)