proposition: Lemma to_of (d:int)(p:positive) : Pos.of_int d = Some p -> Pos.to_int p = norm d.
proof: Proof. unfold Pos.of_int. destruct d; [ | intros [=]]. simpl norm. rewrite <- Unsigned.to_of. destruct (Pos.of_uint d); now intros [= <-]. Qed.
imports: Decimal DecimalFacts PArith NArith