proposition: Lemma to_int_pos_surj d : unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d).
proof: Proof. simpl. unfold Pos.to_int. intros H. destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp). exists p. now f_equal. Qed.
imports: Decimal DecimalFacts PArith NArith