proposition: Lemma arg_maxnP : extremum_spec geq P F arg_max.
proof: Proof. apply: extremumP => //; first exact: leqnn. by move=> n m p mn np; apply: leq_trans mn. by move=> ??; apply: leq_total. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)