From e8560422e88479207893599fbf33a860daa7c5fa Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 31 Oct 2017 14:21:37 +0100
Subject: [PATCH] Provide more Inj instances in numbers

---
 theories/numbers.v | 8 ++++++++
 theories/pretty.v  | 9 +++------
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index 029154f2..80975a32 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -347,6 +347,14 @@ Proof.
 Qed.
 Close Scope Z_scope.
 
+(** * Injectivity of casts *)
+Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
+Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
+Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
+Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
+Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
+(* Add others here. *)
+
 (** * Notations and properties of [Qc] *)
 Open Scope Qc_scope.
 Delimit Scope Qc_scope with Qc.
diff --git a/theories/pretty.v b/theories/pretty.v
index 67dd8fd4..a1e85a46 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2017, Coq-std++ developers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From stdpp Require Export strings.
-From stdpp Require Import relations.
+From stdpp Require Import relations numbers.
 From Coq Require Import Ascii.
 Set Default Proof Using "Type".
 
@@ -72,8 +72,5 @@ Instance pretty_Z : Pretty Z := λ 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.
+Proof. apply _. Qed.
+
-- 
GitLab