proposition: Lemma norm_app_int d d' : nb_digits d' < nb_digits (unorm (app (abs d) d')) -> norm (app_int d d') = app_int (norm d) d'.
proof: Proof. case (uint_eq_dec d' Nil); [now intros->; rewrite !app_int_nil_r|intro Hd']. case d as [d|d]; [now simpl; intro H; apply f_equal, unorm_app_l|]. simpl; unfold unorm. case (uint_eq_dec (nzhead (app d d')) Nil). { intros->; simpl; intro H; exfalso; revert H; apply Nat.le_ngt. now revert Hd'; case d'; [|intros d'' _; apply -> Nat.succ_le_mono; apply Nat.le_0_l..]. } set (m := match nzhead _ with Nil => _ | _ => _ end). intro Ha. replace m with (nzhead (app d d')). 2:{ now unfold m; revert Ha; case nzhead. } intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn). case (uint_eq_dec (app (nzhead d) d') Nil). { intros->; simpl; intro H; exfalso; revert H; apply Nat.le_ngt, Nat.le_0_l. } clear m; set (m := match app _ _ with Nil => _ | _ => _ end). intro Ha'. replace m with (Neg (app (nzhead d) d')); [|now unfold m; revert Ha'; case app]. case (uint_eq_dec (nzhead d) Nil). { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. } clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). intro Hd. now replace m with (Neg (nzhead d)); [|unfold m; revert Hd; case nzhead]. Qed.
imports: Hexadecimal Arith ZArith