proposition: Lemma real_arg_maxP : extremum_spec >=%R P F [arg max_(i > i0 | P i) F i].
proof: Proof. by apply: comparable_arg_maxP => // i j iP jP; rewrite real_comparable ?F_real. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)