proposition: Lemma fnd_fmap0 V k : ([fmap] : {fmap K -> V}).[? k] = None.
proof: Proof. by rewrite not_fnd // in_fset0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)