proposition: Lemma inject_is_additive n m : additive (@inject n m).
proof: Proof. elim: m => [|m ih] //=; rewrite -/(_ \o _). pose iaM := GRing.isAdditive.Build _ _ _ ih. pose iA : GRing.Additive.type _ _ := HB.pack (@inject n m) iaM. have ->: inject m = iA by []. exact: raddfB. 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