diff options
| author | Kazuhiko Sakaguchi | 2020-05-13 13:11:14 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-05-13 14:09:09 +0900 |
| commit | 35bd8708dacfb508f896d957d7b1189ca7decb3e (patch) | |
| tree | 32cfd78b33e69dca564f42df40bfa5a3ec93b4e5 /mathcomp/ssreflect/eqtype.v | |
| parent | 3515b33b1245ea169fbaf61405dc60954509fee2 (diff) | |
Revise proofs in ssreflect/*.v
This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
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)}. |