proposition: Lemma mulrI0_lreg x : (forall y, x * y = 0 -> y = 0) -> lreg x.
proof: Proof. move=> reg_x y z eq_xy_xz; apply/eqP; rewrite -subr_eq0 [y - z]reg_x //. by rewrite mulrBr eq_xy_xz subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)