proposition: Lemma bigmaxf_arg1 f n j: (j < n)%N -> 0 <= f j -> (forall i, (i < n)%N -> f i <= f j) -> \max_(i < n) f i = f j.
proof: Proof. move => js fjp; move / (bigmaxf_lerP f n fjp) => le1. by apply /eqP; rewrite eq_le le1 (bigmaxf_le _ js). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)