proposition: Lemma nzhead_del_tail_nzhead n u : n < nb_digits (nzhead u) -> nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u).
proof: Proof. apply nzhead_del_tail_nzhead_eq, nzhead_involutive. Qed.
imports: Decimal Arith ZArith