proposition: Lemma fnd_rem1 f (k k' : K) : f.[~ k].[? k'] = if k' != k then f.[? k'] else None.
proof: Proof. by rewrite fnd_rem inE; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)