proposition: Lemma raddfMz n : {morph f : x / x *~ n}.
proof: Proof. case: n=> n x /=; first exact: raddfMn. by rewrite NegzE !mulrNz; apply: raddfMNn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)