proposition: Lemma bigmaxf_le0 f n: \max_(i < n) f i <= 0 -> forall i, (i <n)%N -> f i <= 0.
proof: Proof. elim: n => [_ i //| n Hr]; rewrite bigmaxf_rec le_maxl; case /andP => Fk H i. rewrite ltnS leq_eqVlt; case /orP; [ move /eqP ->; apply: Fk | by apply: Hr]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)