proposition: Lemma le_bigmax_ord [x0] n m (P : {pred nat}) (F : nat -> T) : (n <= m)%N -> \big[max/x0]_(i < n | P i) F i <= \big[max/x0]_(i < m | P i) F i.
proof: Proof. exact: le_big_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)