proposition: Lemma gt_size_poly p n : (size p > n)%N -> p != 0.
proof: Proof. by rewrite -size_poly_gt0; apply: leq_trans. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)