fact: Fixpoint del_head n d := match n with | O => d | S n => match d with | Nil => zero | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d | Da d | Db d | Dc d | Dd d | De d | Df d => del_head n d end end.
imports: Datatypes Specif Decimal