proposition: Lemma of_inj_pos d d' : Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'.
proof: Proof. unfold Pos.of_int. destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd'; intros [=]. - apply Unsigned.of_inj; now rewrite Hd, Hd'. - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal. Qed.
imports: Decimal DecimalFacts PArith NArith