proposition: Lemma imset0 : f @: set0 = set0.
proof: Proof. by apply/setP => y /[!inE]; apply/imsetP => -[x /[!inE]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)