proposition: Lemma del_head_app_int_exact i f : nb_digits f < nb_digits (unorm (app (abs i) f)) -> del_head (nb_digits (unorm (app (abs i) f)) - nb_digits f) (unorm (app (abs i) f)) = f.
proof: Proof. simpl; intro Hnb; generalize Hnb; rewrite (unorm_app_l _ _ Hnb); clear Hnb. replace (_ - _) with (nb_digits (unorm (abs i))). - now rewrite del_head_app; [rewrite del_head_nb_digits|]. - rewrite !nb_digits_spec, app_spec, List.app_length. symmetry; apply Nat.add_sub. Qed.
imports: Decimal Arith ZArith