proposition: Lemma catfIs f g h : f + h = g + h -> f.[\ domf h] = g.[\ domf h].
proof: Proof. move=> /fmapP eq_fg_fh; apply/fmapP => k; have := eq_fg_fh k. by rewrite !fnd_cat !fnd_rem; case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)