proposition: Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.
proof: Proof. unfold unorm. split. - generalize (nzhead_nonzero d). destruct nzhead; intros H [=]; trivial. now destruct (H u). - now intros ->. Qed.
imports: Decimal Arith ZArith