proposition: Lemma le_bigmax2 P F1 F2 : (forall i, P i -> F1 i <= F2 i) -> \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i.
proof: Proof. move=> FG; elim/big_ind2 : _ => // a b e f ba fe. rewrite le_max 2!ge_max ba fe /= andbT; have [//|/= af] := leP f a. by rewrite (le_trans ba) // (le_trans _ fe) // ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)