proposition: Lemma del_head_nonnil n u : n < nb_digits u -> del_head n u <> Nil.
proof: Proof. now revert n; induction u; intro n; [|case n; [|intro n'; simpl; intro H; apply IHu, Nat.succ_lt_mono]..]. Qed.
imports: Decimal Arith ZArith