proposition: Lemma bigmaxr_le s F j: j \in s -> F j <= \max_(i <- s) F i.
proof: Proof. elim: s; first by rewrite in_nil. move=> i s IHs Hri0; rewrite big_cons. case Hi: (j == i); first by rewrite (eqP Hi) le_maxr lexx. move: Hri0; rewrite in_cons Hi orFb => ins. by apply: le_trans (IHs ins) _; rewrite le_maxr lexx orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)