fact: Definition int_to_decimal_int (n : Int) : Decimal.int := match n with | neg m => Decimal.Neg (pos_to_uint m) | zero => Decimal.Pos Decimal.Nil | pos m => Decimal.Pos (pos_to_uint m) end.
imports: Basics Spaces.Pos.Core