proposition: Fact fmapP a : fmap a != default (val a).
proof: Proof. rewrite ffunE; have /in_fset_valP [a_in_S] := valP a. by have -> : [` a_in_S] = fincl (fset_sub_val _ _) a by exact/val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)