proposition: Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
proof: Proof. by move=> x y; rewrite -[RHS]oppeK oppe_max !oppeK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed