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