proposition: Lemma bigmaxr_arg1 s F j: j \in s -> 0 <= F j -> (forall i, i \in s -> F i <= F j) -> \max_(i <- s) F i = F j.
proof: Proof. move => js fjp; move / (bigmaxr_lerP s F fjp) => le1. by apply /eqP; rewrite eq_le le1 (bigmaxr_le _ js). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)