proposition: Lemma bigmaxf_ge0 f n: 0 <= \max_(i < n) f i.
proof: Proof. elim: n => [| n IHn]; first by rewrite big_ord0. by rewrite bigmaxf_rec le_maxr IHn orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)