proposition: Lemma nztail_spec d : let (r, n) := nztail d in let (r', n') := lnztail (to_list d) in to_list r = r' /\ n = n'.
proof: Proof. unfold nztail, lnztail. set (f := fix aux d_rev := match d_rev with | D0 d_rev => let (r, n) := aux d_rev in (r, S n) | _ => (d_rev, 0) end). set (f' := fix aux (l_rev : list digits) : list digits * nat := match l_rev with | cons d0 l_rev => let (r, n) := aux l_rev in (r, S n) | _ => (l_rev, 0) end). rewrite <-(of_list_to_list (rev d)), rev_spec. induction (List.rev _) as [|h t IHl]; [now simpl|]. case h; simpl; [|now rewrite rev_spec; simpl; rewrite to_list_of_list..]. now revert IHl; case f; intros r n; case f'; intros r' n' [-> ->]. Qed.
imports: Decimal Arith ZArith