proposition: Lemma unorm_app_r d d' : nb_digits (unorm (app d d')) <= nb_digits d' -> unorm (app d d') = unorm d'.
proof: Proof. case (uint_eq_dec (nzhead (app d d')) Nil). { now unfold unorm; intro H; rewrite H, (nzhead_app_nil_r _ _ H). } intro Ha; rewrite (unorm_nzhead _ Ha). case (uint_eq_dec (nzhead d') Nil). { now intros H H'; exfalso; apply Ha; rewrite nzhead_app_r. } intro Hd'; rewrite (unorm_nzhead _ Hd'); apply nzhead_app_r. Qed.
imports: Decimal Arith ZArith