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