proposition: Lemma fmorph_inj : injective f.
proof: Proof. by apply/raddf_inj => x /eqP; rewrite fmorph_eq0 => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)