proposition: Lemma catf_reml A f g : f.[\ A] + g = (f + g).[\ A `\` domf g].
proof: Proof. by apply/fmapP=> k; rewrite !(fnd_cat, fnd_rem) inE; case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)