proposition: Lemma extremum_inP : extremum_spec ord P F (extremum ord i0 P F).
proof: Proof. rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i]. by split=> // j; apply/implyP. pose TP := seq_sub [seq F i | i <- enum P]. have FPP (iP : {i | P i}) : F (proj1_sig iP) \in [seq F i | i <- enum P]. by rewrite map_f// mem_enum; apply: valP. pose FP := SeqSub (FPP _). have []//= := @extremumP _ _ (relpre val ord) (exist P i0 Pi0) xpredT FP. - by move=> [/= _/mapP[i iP ->]]; apply: ord_refl; rewrite mem_enum in iP. - move=> [/= _/mapP[j jP ->]] [/= _/mapP[i iP ->]] [/= _/mapP[k kP ->]]. by apply: ord_trans; rewrite !mem_enum in iP jP kP. - move=> [/= _/mapP[i iP ->]] [/= _/mapP[j jP ->]]. by apply: ord_total; rewrite !mem_enum in iP jP. - rewrite /FP => -[/= i Pi] _ /(_ (exist _ _ _))/= ordF. have /negP/negP/= := no_i i; rewrite Pi/= negb_forall => /existsP/sigW[j]. by rewrite negb_imply => /andP[Pj]; rewrite ordF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)