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.

---
 CHANGELOG_UNRELEASED.md      | 3 +++
 mathcomp/ssreflect/fintype.v | 4 +++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 86c920b..db1c642 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -319,6 +319,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + `>=< y` stands for `[pred x | x >=< y]`
 
 - in `ssrint.v`, generalized `mulpz` for any `ringType`.
+- In `fintype.v`, lemmas `inj_card_onto` and `inj_card_bij` take a
+  weaker hypothesis (i.e. `#|T| >= #|T'|` instead of `#|T| = #|T'|`
+  thanks to `leq_card` under injectivity assumption).
 
 ### Renamed
 
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