proposition: Lemma bigmaxf_arg f n : {j | (j <n)%N & 0 <= f j} -> {j | (j <n)%N & \max_(i < n) f i = f j}.
proof: Proof. elim:n => [ [j] // | n Hr Hf]; rewrite bigmaxf_rec. case (lerP (\max_(i < n) f i) (f n)) => cmpm. by exists n => //; apply /eqP; rewrite eqr_maxl. move: (ltW cmpm); rewrite - eq_maxr/=; move /eqP => <-. suff aux: { j | (j < n)%N & 0 <= f j}. move: (Hr aux) => [j jl jm]; exists j. by rewrite ltnS ltnW. rewrite /Num.max/= jm; case: ifPn => //. by rewrite -jm cmpm. move: Hf => [j]; rewrite ltnS leq_eqVlt. case e: (j == n); last by rewrite orFb; exists j => //. rewrite (eqP e) => _ h2; move: (le_lt_trans h2 cmpm) => aux. by move: (bigmaxf_gt0 aux) =>[k ja jb]; exists k =>//; apply: ltW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)