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