proposition: Lemma nzhead_del_tail_nzhead_eq n u : nzhead u = u -> n < nb_digits u -> nzhead (del_tail n u) = del_tail n u.
proof: Proof. rewrite nb_digits_spec, <-List.rev_length. intros Hu Hn. apply to_list_inj; unfold del_tail. rewrite nzhead_spec, rev_spec. rewrite del_head_spec_small; [|now rewrite rev_spec; apply Nat.lt_le_incl]. rewrite rev_spec. rewrite List.skipn_rev, List.rev_involutive. generalize (f_equal to_list Hu) Hn; rewrite nzhead_spec; intro Hu'. case (to_list u) as [|h t]. { simpl; intro H; exfalso; revert H; apply Nat.le_ngt, Nat.le_0_l. } intro Hn'; generalize (Nat.sub_gt _ _ Hn'); rewrite List.rev_length. case (_ - _); [now simpl|]; intros n' _. rewrite List.firstn_cons, lnzhead_head_nd0; [now simpl|]. intro Hh; revert Hu'; rewrite Hh; apply lnzhead_neq_d0_head. Qed.
imports: Decimal Arith ZArith