proposition: Lemma dnorm_i_exact i f : (nb_digits f < nb_digits (unorm (app (abs i) f)))%nat -> match i with | Pos i => Pos (unorm i) | Neg i => match nzhead (app i f) with | Nil => Pos zero | _ => Neg (unorm i) end end = norm i.
proof: Proof. case i as [ni|ni]; [now simpl|]; simpl. case (uint_eq_dec (nzhead (app ni f)) Nil); intro Ha. { now rewrite Ha, (nzhead_app_nil_l _ _ Ha). } rewrite (unorm_nzhead _ Ha). set (m := match nzhead _ with Nil => _ | _ => _ end). replace m with (Neg (unorm ni)); [|now unfold m; revert Ha; case nzhead]. case (uint_eq_dec (nzhead ni) Nil); intro Hni. { rewrite <-nzhead_app_nzhead, Hni, app_nil_l. intro H; exfalso; revert H; apply Nat.le_ngt, nb_digits_nzhead. } clear m; set (m := match nzhead ni with Nil => _ | _ => _ end). replace m with (Neg (nzhead ni)); [|now unfold m; revert Hni; case nzhead]. now rewrite (unorm_nzhead _ Hni). Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith