fact: Fixpoint of_lu (d:uint) : nat := match d with | Nil => 0 | D0 d => 10 * of_lu d | D1 d => 1 + 10 * of_lu d | D2 d => 2 + 10 * of_lu d | D3 d => 3 + 10 * of_lu d | D4 d => 4 + 10 * of_lu d | D5 d => 5 + 10 * of_lu d | D6 d => 6 + 10 * of_lu d | D7 d => 7 + 10 * of_lu d | D8 d => 8 + 10 * of_lu d | D9 d => 9 + 10 * of_lu d end.
imports: Decimal DecimalFacts Arith