proposition: Lemma intmul1_is_multiplicative : multiplicative ( *~%R (1 : R)).
proof: Proof. by split; move=> // x y /=; rewrite ?intrD ?mulrNz ?intrM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)