proposition: Lemma dnorm_i_exact' i f : (nb_digits (unorm (app (abs i) f)) <= nb_digits 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 = match norm (app_int i f) with | Pos _ => Pos zero | Neg _ => Neg zero end.
proof: Proof. case i as [ni|ni]; simpl. { now intro Hnb; rewrite (unorm_app_zero _ _ Hnb). } unfold unorm. case (uint_eq_dec (nzhead (app ni f)) Nil); intro Hn. { now rewrite Hn. } set (m := match nzhead _ with Nil => _ | _ => _ end). replace m with (nzhead (app ni f)). 2:{ now unfold m; revert Hn; case nzhead. } clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). replace m with (Neg (unorm ni)). 2:{ now unfold m, unorm; revert Hn; case nzhead. } clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). replace m with (Neg (nzhead (app ni f))). 2:{ now unfold m; revert Hn; case nzhead. } rewrite <-(unorm_nzhead _ Hn). now intro H; rewrite (unorm_app_zero _ _ H). Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith