proposition: Lemma app_int_del_tail_head n (d:int) : n <= nb_digits (abs d) -> app_int (del_tail_int n d) (del_head (nb_digits (abs d) - n) (abs d)) = d.
proof: Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed.
imports: Decimal Arith ZArith