From aad2327376b2f76950be51a6bf22b32b0a01b2eb Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 30 Oct 2020 19:42:56 +0100
Subject: Generalizing inj_card_onto and inj_card_bij.

---
 mathcomp/ssreflect/fintype.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 422d760..91d5c80 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1300,7 +1300,9 @@ Qed.
 
 Lemma leq_card : #|T| <= #|T'|. Proof. exact: (leq_card_in (in2W _)). Qed.
 
-Hypothesis card_range : #|T| = #|T'|.
+Hypothesis card_range : #|T| >= #|T'|.
+
+Let eq_card : #|T| = #|T'|. Proof. by apply/eqP; rewrite eqn_leq leq_card. Qed.
 
 Lemma inj_card_onto y : y \in codom f.
 Proof. by move: y; apply/subset_cardP; rewrite ?card_codom ?subset_predT. Qed.
-- 
cgit v1.2.3