proposition: Lemma unorm_app_l d d' : nb_digits d' < nb_digits (unorm (app d d')) -> unorm (app d d') = app (unorm d) d'.
proof: Proof. case (uint_eq_dec d' Nil); [now intros->; rewrite !app_nil_r|intro Hd']. case (uint_eq_dec (nzhead (app d d')) Nil). { unfold unorm; intros->; simpl; intro H; exfalso; revert H; apply Nat.le_ngt. now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. } intro Ha; rewrite (unorm_nzhead _ Ha). intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn). rewrite !nb_digits_spec, app_spec, List.app_length. case (uint_eq_dec (nzhead d) Nil). { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. } now intro H; rewrite (unorm_nzhead _ H). Qed.
imports: Decimal Arith ZArith