proposition: Lemma app_spec d d' : to_list (app d d') = Datatypes.app (to_list d) (to_list d').
proof: Proof. unfold app. now rewrite revapp_spec, List.rev_append_rev, rev_spec, List.rev_involutive. Qed.
imports: Decimal Arith ZArith