proposition: Lemma arg_minnP : extremum_spec leq P F arg_min.
proof: Proof. by apply: extremumP => //; [apply: leq_trans|apply: leq_total]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)