diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrfun.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |