proposition: Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
proof: Proof. move=> y z; rewrite -![x *~ _]mulrzr => /(mulfI hx). by apply: inc_inj y z; exact: ler_pMz2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)