proposition: Lemma bigmaxf_le f n j: (j < n)%N -> f j <= \max_(i < n) f i.
proof: Proof. elim: n => [ //| n IHn]; rewrite bigmaxf_rec. case Hi: (j == n); first by rewrite (eqP Hi) le_maxr lexx. rewrite ltnS leq_eqVlt Hi orFb => aux;apply: (le_trans (IHn aux)). by rewrite le_maxr lexx orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)