proposition: Lemma fscompE g f : (g \o f)%fsfun =1 g \o f.
proof: Proof. move=> k; rewrite fsfun_ffun; case: insubP => //= [u _ <- //|]. by rewrite inE => /norP [kNf kNg]; rewrite !fsfun_dflt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)