proposition: Lemma fsfun0_inj : injective default -> injective [fsfun for default].
proof: Proof. by move=> def_inj x y; rewrite !fsfunE => /def_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)