proposition: Lemma polyC_eqp1 (c : R) : (c%:P %= 1) = (c != 0).
proof: Proof. apply/eqpP/idP => [[[x y]] |nc0] /=. case: (eqVneq c) => [->|] //= /andP [_] /negPf <- /eqP. by rewrite alg_polyC scaler0 eq_sym polyC_eq0. exists (1, c); first by rewrite nc0 /= oner_neq0. by rewrite alg_polyC scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)