proposition: Lemma set_0Vmem A : (A = set0) + {x : T | x \in A}.
proof: Proof. case: (pickP (mem A)) => [x Ax | A0]; [by right; exists x | left]. by apply/setP=> x; rewrite in_set; apply: A0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)