proposition: Lemma fnd_rem f A (k : K) : f.[\ A].[? k] = if k \in A then None else f.[? k].
proof: Proof. rewrite fnd_restrict inE. by case: fndP => ?; rewrite ?(andbT, andbF) //=; case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)