proposition: Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.
proof: Proof. move=> [x| |] [y| |] //=. - by rewrite -fine_max//= -fine_min//= oppr_max. - by rewrite maxey mineNy. - by rewrite miney. - by rewrite minNye. - by rewrite maxNye minye. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed