fact: Fixpoint to_list (u : uint) : list digits := match u with | Nil => nil | D0 u => cons d0 (to_list u) | D1 u => cons d1 (to_list u) | D2 u => cons d2 (to_list u) | D3 u => cons d3 (to_list u) | D4 u => cons d4 (to_list u) | D5 u => cons d5 (to_list u) | D6 u => cons d6 (to_list u) | D7 u => cons d7 (to_list u) | D8 u => cons d8 (to_list u) | D9 u => cons d9 (to_list u) end.
imports: Decimal Arith ZArith