proposition: Lemma cat0f f : [fmap] + f = f.
proof: Proof. apply/fmapP => k; rewrite fnd_cat; case: ifPn => //= kf. by rewrite !not_fnd ?inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)