proposition: Lemma num_max : {morph num : x y / Order.max x y}.
proof: Proof. by move=> x y; rewrite !maxEle num_le -fun_if. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)