fact: Definition itv_bound_signr (b : itv_bound int) : KnownSign.sign := let b0 := BRight 0%Z in (if b == b0 then =0 else if (b <= b0)%O then <=0 else >=0)%snum_sign.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed