proposition: Lemma norm_involutive d : norm (norm d) = norm d.
proof: Proof. unfold norm. destruct d. - f_equal. apply unorm_involutive. - destruct (nzhead d) eqn:E; auto. destruct (nzhead_nonzero _ _ E). Qed.
imports: Decimal Arith ZArith