proposition: Lemma codomf_cat (f g : {fmap K -> V}) : codomf (f + g) = codomf g `|` codomf f.[\domf g].
proof: Proof. apply/fsetP => v'; rewrite !inE. apply/codomfP/(orPP (codomfP _ _) (codomfP _ _)); last first. move=> [] [x xI]; exists x; rewrite fnd_cat; first by case: fndP xI. by move: xI; rewrite fnd_rem; case: ifP. move=> []x; rewrite fnd_cat; case: fndP => // [xg gx|xNg fx]. by left; exists x; rewrite in_fnd. by right; exists x; rewrite fnd_rem ifN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)