proposition: Lemma to_uint_inj p p' : Pos.to_uint p = Pos.to_uint p' -> p = p'.
proof: Proof. intro E. assert (E' : N.pos p = N.pos p'). { now rewrite <- (of_to p), <- (of_to p'), E. } now injection E'. Qed.
imports: Decimal DecimalFacts PArith NArith