proposition: Lemma bigmaxr_gt0 s F: \max_(i <- s) F i > 0 -> { i | i \in s & F i > 0}.
proof: Proof. elim :s => [| a l Hrec]; first by rewrite big_nil ltxx. rewrite big_cons lt_maxr. case (ltrP 0 (F a)); first by exists a => //; rewrite in_cons eqxx. rewrite leNgt => /negbTE ->; rewrite orFb => /Hrec [b bl fp0]. by exists b => //;rewrite in_cons bl orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)