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