proposition: Lemma del_head_spec_large n d : length (to_list d) < n -> del_head n d = zero.
proof: Proof. revert d; induction n; intro d; [now case d|]. now case d; [|intro d'; simpl; intro H; rewrite (IHn _ (proj2 (Nat.succ_lt_mono _ _) H))..]. Qed.
imports: Decimal Arith ZArith