diff --git a/theories/pretty.v b/theories/pretty.v
index 541e72a23363bf660fcb8496874fb7414e8ab614..67dd8fd48daec28a4cb86f895d1a8666814d0a10 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -70,3 +70,10 @@ Instance pretty_Z : Pretty Z := λ x,
   match x with
   | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
   end%string.
+Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
+Instance pretty_nat_inj : Inj (@eq nat) (=) pretty.
+Proof.
+  unfold pretty, pretty_nat.
+  apply compose_inj with (R2 := eq) (f := N.of_nat), _.
+  exact Nat2N.inj.
+Qed.