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