proposition: Lemma mulrIn x : x != 0 -> injective (GRing.natmul x).
proof: Proof. move=> x_neq0 m n; without loss /subnK <-: m n / (n <= m)%N. by move=> IH eq_xmn; case/orP: (leq_total m n) => /IH->. by move/eqP; rewrite mulrnDr -subr_eq0 addrK mulrn_eq0 => /predU1P[-> | /idPn]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)