proposition: Lemma bigmaxr_ge0 s F: 0 <= \max_(i <- s) F i.
proof: Proof. elim: s; first by rewrite big_nil. by move=> s IHs Hri0; rewrite big_cons le_maxr Hri0 orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)