proposition: Lemma rmodp1 p : rmodp p 1 = 0.
proof: Proof. apply/eqP; have := ltn_rmodp p 1. by rewrite !oner_neq0 -size_poly_eq0 size_poly1 ltnS leqn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)