proposition: Lemma rdvdp1 d : rdvdp d 1 = (size d == 1).
proof: Proof. rewrite /rdvdp; have [->|] := eqVneq d 0. by rewrite rmodp0 size_poly0 (negPf (oner_neq0 _)). rewrite -size_poly_leq0 -ltnS; case: ltngtP => // [|/eqP] hd _. by rewrite rmodp_small ?size_poly1 // oner_eq0. have [c cn0 ->] := size_poly1P _ hd. rewrite /rmodp unlock -size_poly_eq0 size_poly1 /= size_poly1 size_polyC cn0 /=. by rewrite polyC_eq0 (negPf cn0) !lead_coefC !scale1r subrr !size_poly0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)