proposition: Lemma of_to (n:N) : N.of_int (N.to_int n) = Some n.
proof: Proof. unfold N.to_int, N.of_int, norm. f_equal. rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. Qed.
imports: Decimal DecimalFacts DecimalPos PArith NArith