proposition: Lemma inject_is_multiplicative n m : multiplicative (@inject n m).
proof: Proof. elim: m => [|m ih] //=; rewrite -/(_ \o _). pose imM := GRing.isMultiplicative.Build _ _ _ ih. pose iM : GRing.RMorphism.type _ _ := HB.pack (@inject n m) imM. have ->: inject m = iM by []. exact: (rmorphM _, rmorph1 _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg