proposition: Lemma fnd_set V (f : {fmap K -> V}) k0 v0 k : f.[k0 <- v0].[? k] = if k == k0 then Some v0 else f.[? k].
proof: Proof. case: fndP => [ksf|]; last first. by rewrite mem_setf inE negb_or => /andP [/negPf ->]; case: fndP. rewrite setfK; case: eqP => [kNk0|/negPn/=]; last by rewrite negbK => ->. by rewrite Some_fnd (negPf kNk0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)