proposition: Lemma to_of (d:int)(n:N) : N.of_int d = Some n -> N.to_int n = norm d.
proof: Proof. unfold N.of_int. destruct (norm d) eqn:Hd; intros [= <-]. unfold N.to_int. rewrite Unsigned.to_of. f_equal. revert Hd; destruct d; simpl. - intros [= <-]. apply unorm_involutive. - destruct (nzhead d); now intros [= <-]. Qed.
imports: Decimal DecimalFacts DecimalPos PArith NArith