proposition: Lemma remf_set f A (k : K) (v : V) : f.[k <- v].[\ A] = if k \in A then f.[\ A] else f.[\ A].[k <- v].
proof: Proof. apply/fmapP => k' /=; rewrite !(fnd_if, fnd_rem, fnd_set, inE). by case: eqP => [->|]; do !case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)