proposition: Lemma Fmin_correct : extremum_spec leq Fmin.
proof: Proof. rewrite /Fmin; case: pickP => [i | no_i] /=. by case/andP=> Pi; move/forallP=> min_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. case/ex_minnP: exFval=> m; case/existsP=> j; case/andP=> Pj e m_is_min. case/idP: (no_i j); rewrite /= Pj; apply/forallP=> x; apply/implyP=> Px. by rewrite (eqP e); apply: m_is_min; apply/existsP; exists x; rewrite eqxx Px. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)