proposition: Lemma del_tail_app_int_exact i f : nb_digits f < nb_digits (unorm (app (abs i) f)) -> del_tail_int (nb_digits f) (norm (app_int i f)) = norm i.
proof: Proof. simpl; intro Hnb. rewrite (norm_app_int _ _ Hnb). rewrite del_tail_app_int; [|now simpl]. now rewrite del_tail_nb_digits, app_int_nil_r. Qed.
imports: Decimal Arith ZArith