proposition: Lemma lee_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x <= y}.
proof: Proof. move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !lerN2. by rewrite /Order.le/= realN. by rewrite /Order.le/= realN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed