proposition: Lemma polyd0 (F: nat -> R): \poly_(i < 0) (F i) = 0.
proof: Proof. apply /eqP;rewrite - size_poly_eq0; rewrite - leqn0; exact: (size_poly 0 F). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)