fact: Definition int_of_decimal_int (d : Decimal.int) : Int := match d with | Decimal.Pos u => int_of_decimal_uint u | Decimal.Neg u => let t := int_of_decimal_uint u in match t with | pos v => neg v | _ => zero end end.
imports: Basics Spaces.Pos.Core