proposition: Lemma mulfI x : x != 0 -> injective ( *%R x).
proof: Proof. move=> nz_x y z; apply: contra_eq => neq_yz. by rewrite -subr_eq0 -mulrBr mulf_neq0 ?subr_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)