fact: Definition reality_cond (n : reality) (x : T) := match n with | Real (Sign EqZero) => x == x0 | Real (Sign NonNeg) => x >= x0 | Real (Sign NonPos) => x <= x0 | Real AnySign => (x0 <= x) || (x <= x0) | Arbitrary => true end.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)