proposition: Lemma norm_del_tail_int_norm n d : n < nb_digits (match norm d with Pos d | Neg d => d end) -> norm (del_tail_int n (norm d)) = del_tail_int n (norm d).
proof: Proof. case d; clear d; intros u; simpl. - now intro H; simpl; rewrite unorm_del_tail_unorm. - case (uint_eq_dec (nzhead u) Nil); intro Hu. + now rewrite Hu; case n; [|intros n' Hn'; generalize (proj2 (Nat.succ_lt_mono _ _) Hn')]. + set (m := match nzhead u with Nil => Pos zero | _ => _ end). replace m with (Neg (nzhead u)); [|now unfold m; revert Hu; case nzhead]. unfold del_tail_int. clear m Hu. simpl. intro H; generalize (del_tail_nonnil _ _ H). rewrite (nzhead_del_tail_nzhead _ _ H). now case del_tail. Qed.
imports: Decimal Arith ZArith