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