proposition: Lemma bigmaxf_gt0 f n: \max_(i < n ) f i > 0 -> { i | (i <n)%N & f i > 0}.
proof: Proof. elim :n => [| a IH]; first by rewrite big_ord0 ltxx. case (ltrP 0 (f a)); first by exists a. rewrite bigmaxf_rec lt_maxr leNgt; move /negbTE => ->; rewrite orFb => aux. by move: (IH aux) => [b bl fp0]; exists b => //; apply:ltn_trans (ltnSn a). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)