proposition: Lemma del_tail_nonnil n u : n < nb_digits u -> del_tail n u <> Nil.
proof: Proof. unfold del_tail. rewrite <-nb_digits_rev. generalize (rev u); clear u; intro u. intros Hu H. generalize (rev_nil_inv _ H); clear H. now apply del_head_nonnil. Qed.
imports: Decimal Arith ZArith