From 45940df1c68ba8b4546c5ae0c7e464505a7f0ad6 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Thu, 14 Nov 2019 17:58:19 +0300
Subject: fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from
 fintype (#403)

---
 mathcomp/ssreflect/fingraph.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 70536dc..671bb95 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -543,9 +543,6 @@ Lemma f_finv : cancel finv f. Proof. exact: (in1T (f_finv_in _ (in2W _))). Qed.
 
 Lemma finv_f : cancel f finv. Proof. exact: (in1T (finv_f_in _ (in2W _))). Qed.
 
-Lemma fin_inj_bij : bijective f.
-Proof. by exists finv; [apply: finv_f|apply: f_finv]. Qed.
-
 Lemma finv_bij : bijective finv.
 Proof. by exists f; [apply: f_finv|apply: finv_f]. Qed.
 
@@ -643,7 +640,7 @@ Variables (T : finType) (f f' : T -> T).
 Lemma finv_eq_can : cancel f f' -> finv f =1 f'.
 Proof.
 move=> fK; have inj_f := can_inj fK.
-by apply: bij_can_eq fK; [apply: fin_inj_bij | apply: finv_f].
+by apply: bij_can_eq fK; [apply: injF_bij | apply: finv_f].
 Qed.
 
 Hypothesis eq_f : f =1 f'.
-- 
cgit v1.2.3