proposition: Lemma codomf0 : codomf [fmap] = fset0.
proof: Proof. apply/fsetP=> k; rewrite inE; apply/negP => /codomfP [k']. by rewrite not_fnd //= inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)