proposition: Lemma eqp_scale p c : c != 0 -> c *: p %= p.
proof: Proof. move=> c0; apply/eqpP; exists (1, c); first by rewrite c0 oner_eq0. by rewrite scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)