proposition: Lemma fine_max : {in fin_num &, {mono @fine R : x y / maxe x y >-> (Num.max x y)%:E}}.
proof: Proof. by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y; [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed