Require Import Decimal.

Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.

Lemma rev_revapp d d' :
 rev (revapp d d') = revapp d' d.

Lemma rev_rev d : rev (rev d) = d.

Fixpoint nztail d :=
 match d with
 | Nil => Nil
 | D0 d => match nztail d with Nil => Nil | d' => D0 d' end
 | D1 d => D1 (nztail d)
 | D2 d => D2 (nztail d)
 | D3 d => D3 (nztail d)
 | D4 d => D4 (nztail d)
 | D5 d => D5 (nztail d)
 | D6 d => D6 (nztail d)
 | D7 d => D7 (nztail d)
 | D8 d => D8 (nztail d)
 | D9 d => D9 (nztail d)
 end.

Definition lnorm d :=
 match nztail d with
 | Nil => zero
 | d => d
 end.

Lemma nzhead_revapp_0 d d' : nztail d = Nil ->
 nzhead (revapp d d') = nzhead d'.

Lemma nzhead_revapp d d' : nztail d <> Nil ->
 nzhead (revapp d d') = revapp (nztail d) d'.

Lemma nzhead_rev d : nztail d <> Nil ->
 nzhead (rev d) = rev (nztail d).

Lemma rev_nztail_rev d :
  rev (nztail (rev d)) = nzhead d.

Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.

Lemma rev_nil_inv d : rev d = Nil -> d = Nil.

Lemma rev_lnorm_rev d :
  rev (lnorm (rev d)) = unorm d.

Lemma nzhead_nonzero d d' : nzhead d <> D0 d'.

Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.

Lemma unorm_nonnil d : unorm d <> Nil.

Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.

Lemma unorm_invol d : unorm (unorm d) = unorm d.

Lemma norm_invol d : norm (norm d) = norm d.