proposition: Lemma intmul_inj: injective(fun z:nat => (@intmul int 1%Z z)).
proof: Proof. by move=> a b /=; rewrite !intz => sf; injection sf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)