proposition: Lemma unorm_app_zero d d' : nb_digits (unorm (app d d')) <= nb_digits d' -> unorm d = zero.
proof: Proof. unfold unorm. case (uint_eq_dec (nzhead (app d d')) Nil). { now intro Hn; rewrite Hn, (nzhead_app_nil_l _ _ Hn). } intro H; fold (unorm (app d d')); rewrite (unorm_nzhead _ H); intro H'. case (uint_eq_dec (nzhead d) Nil); [now intros->|]. intro H''; fold (unorm d); rewrite (unorm_nzhead _ H''). exfalso; apply H''; revert H'; apply nzhead_app_nil. Qed.
imports: Decimal Arith ZArith