proposition: Fact fsfun_subproof (f : fsfun) : forall (k : K) (kf : k \in fmap_of_fsfun f), (fmap_of_fsfun f).[kf]%fmap != default k.
proof: Proof. case:f => f f_stable k kf /=. exact: (forallP f_stable [` kf]). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)