proposition: Lemma bigmaxr_le0 s F: \max_(i <- s) F i <= 0 -> forall i, i \in s -> F i <= 0.
proof: Proof. elim: s; first by move=> _ i;rewrite in_nil. move=> k s IHs; rewrite big_cons le_maxl; case /andP => Fk Hr1 i. rewrite in_cons; case /orP; [ move /eqP ->; apply: Fk | by apply: IHs]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)