proposition: Lemma bigmaxf_lerP f n m: m >= 0 -> reflect (forall i, (i < n)%N -> f i <= m) (\max_(i <n) f i <= m).
proof: Proof. move=> h; apply: (iffP idP) => leFm => [i ir | ]. by apply: le_trans leFm; apply: bigmaxf_le. rewrite big_seq_cond; elim /big_ind:_ => //. by move=> x y xm ym; rewrite le_maxl; apply /andP. by move=> [i hi] _; apply: leFm. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)