proposition: Lemma of_int_norm d : Pos.of_int (norm d) = Pos.of_int d.
proof: Proof. unfold Pos.of_int. destruct d. - simpl. now rewrite Unsigned.of_uint_norm. - simpl. now destruct (nzhead d) eqn:H. Qed.
imports: Decimal DecimalFacts PArith NArith