proposition: Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i) (m < \big[max/x]_(i | P i) F i).
proof: Proof. apply: (iffP idP) => [|[mx|[i Pi mFi]]]. - rewrite ltNge => /bigmax_leP /not_andP[/negP|]; first by rewrite -ltNge; left. by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i. - by rewrite bigmax_idl lt_maxr mx. - by rewrite (bigmaxD1 i)// lt_maxr mFi. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed