proposition: Lemma del_head_spec_small n d : n <= length (to_list d) -> to_list (del_head n d) = List.skipn n (to_list d).
proof: Proof. revert d; induction n as [|n IHn]; intro d; [now simpl|]. now case d; [|intros d' H; apply IHn, le_S_n..]. Qed.
imports: Decimal Arith ZArith