proposition: Lemma app_del_tail_head n (d:uint) : n <= nb_digits d -> app (del_tail n d) (del_head (nb_digits d - n) d) = d.
proof: Proof. rewrite nb_digits_spec; intro Hn; unfold del_tail. rewrite <-(of_list_to_list (app _ _)), app_spec, rev_spec. rewrite del_head_spec_small; [|now rewrite rev_spec, List.rev_length]. rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. rewrite rev_spec. set (n' := _ - n). assert (Hn' : n = length (to_list d) - n'). { now rewrite <- (Nat.add_sub (length (to_list d)) n), Nat.add_comm, <- 2 Nat.add_sub_assoc, Nat.sub_diag; trivial. } now rewrite Hn', <-List.firstn_skipn_rev, List.firstn_skipn, of_list_to_list. Qed.
imports: Decimal Arith ZArith