proposition: Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m) (\big[min/x]_(i | P i) F i <= m).
proof: Proof. apply: (iffP idP) => [|[xm|[i Pi Fim]]]. - rewrite leNgt => /bigmin_gtP /not_andP[/negP|]; first by rewrite -leNgt; left. by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i. - by rewrite bigmin_idl le_minl xm. - by rewrite (bigminD1 i)// le_minl Fim. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed