diff options
| author | affeldt-aist | 2020-05-28 16:24:38 +0200 |
|---|---|---|
| committer | GitHub | 2020-05-28 16:24:38 +0200 |
| commit | 5c67ea2530ba6aaa0dbffaa41e037cfdc9345d00 (patch) | |
| tree | bb22445744384365f6766578a01fae1d5240a81e /mathcomp/ssreflect/eqtype.v | |
| parent | 14291b88255b7a1a110c21dec5a3754f25ec8881 (diff) | |
| parent | 37a49513f22a3f792a1ac3241962a7d17455f7e5 (diff) | |
Merge pull request #504 from pi8027/selectors
Revise proofs in ssreflect/*.v
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 12b0601..bd58e01 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -409,7 +409,7 @@ Lemma bij_eq : bijective f -> forall x y, (f x == f y) = (x == y). Proof. by move/bij_inj; apply: inj_eq. Qed. Lemma can2_eq : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y). -Proof. by move=> fK gK x y; rewrite -{1}[y]gK; apply: can_eq. Qed. +Proof. by move=> fK gK x y; rewrite -[y in LHS]gK; apply: can_eq. Qed. Lemma inj_in_eq : {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}. |