proposition: Lemma bigmaxr_arg s F: {j | j \in s & 0 <= F j} -> {j | j \in s & \max_(i <- s) F i = F j}.
proof: Proof. elim:s; first by case => w ;rewrite in_nil. move => a l Hrec ew; rewrite big_cons. case (lerP (\max_(i <- l) F i) (F a)) => cmpm. by exists a; [ rewrite in_cons eqxx | apply /eqP; rewrite eq_maxl]. move: (ltW cmpm); rewrite - eq_maxr; move /eqP => ->. suff aux: { w : R | w \in l & 0 <= F w}. move: (Hrec aux) => [j jl jm]; exists j =>//; rewrite in_cons jl orbT//. move: ew => [w]; rewrite in_cons => h1 h2. case e: (w == a); last first. exists w => //; move: h1; case /orP => //; rewrite e //. rewrite (eqP e) in h2; move: (le_lt_trans h2 cmpm) => aux. by move: (bigmaxr_gt0 aux) =>[j ja jb]; exists j =>//; apply: ltW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)