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