fact: CoInductive posnum_spec (R : numDomainType) (x : R) : R -> bool -> bool -> bool -> Type := | IsPosnum (p : {posnum R}) : posnum_spec x (p%:num) false true true.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)