proposition: Lemma catf_rem1l k f g : f.[~ k] + g = if k \in g then f + g else (f + g).[~ k].
proof: Proof. apply/fmapP => k'; rewrite !(fnd_if, fnd_cat, fnd_rem1). by have [->|?] := altP eqP; do !case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)