proposition: Lemma extremumP : extremum_spec ord P F extremum.
proof: Proof. rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i]. by split=> // j; apply/implyP. have := sort_sorted ord_total [seq F i | i <- enum P]. set s := sort _ _ => ss; have s_gt0 : size s > 0 by rewrite size_sort size_map -cardE; apply/card_gt0P; exists i0. pose t0 := nth (F i0) s 0; have: t0 \in s by rewrite mem_nth. rewrite mem_sort => /mapP/sig2_eqW[it0]; rewrite mem_enum => it0P def_t0. have /negP[/=] := no_i it0; rewrite [P _]it0P/=; apply/'forall_implyP=> j Pj. have /(nthP (F i0))[k g_lt <-] : F j \in s by rewrite mem_sort map_f ?mem_enum. by rewrite -def_t0 sorted_leq_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)