proposition: Lemma Fmax_correct : extremum_spec geq Fmax.
proof: Proof. rewrite /Fmax; case: pickP => [i | no_i]. by case/andP=> Pi; move/forallP=> max_i; split=> // j; exact/implyP. pose Fvals i := [exists x, P x && (F x == i)]. have exFval : exists n, Fvals n. by exists (F i0); rewrite /Fvals; apply/existsP; exists i0; rewrite Pi0 eqxx. have: forall n, Fvals n -> n <= foldr maxn 0 (map F (enum P)). move=> n; case/existsP=> i; rewrite -[P i]mem_enum andbC; case/andP. move/eqP <-; elim: (enum P) => //= j e IHe. rewrite inE => /orP[/eqP->|/IHe /leq_trans->//]; first by rewrite leq_maxl. exact: leq_maxr. case/ex_maxnP=> // n ex_i max_i; case/pred0P: ex_i => i. apply/andP=> [[Pi def_n]]; case/idP: (no_i i); rewrite /= Pi. apply/forallP=> j; apply/implyP=> Pj; rewrite (eqP def_n) max_i //;apply/existsP. by exists j; rewrite eqxx Pj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)