From 6acef5bb290837871337983037833dad29606d79 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 22 Nov 2019 11:07:28 +0100
Subject: Added ssrfun theorem `inj_compr` (#432)

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

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index de917a9..f189dcb 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -17,3 +17,7 @@ Definition of_void T (x : void) : T := match x with end.
 
 Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
 Proof. by case. Qed.
+
+Lemma inj_compr A B C (f : B -> A) (h : C -> B) :
+   injective (f \o h) -> injective h.
+Proof. by move=> fh_inj x y /(congr1 f) /fh_inj. Qed.
-- 
cgit v1.2.3