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/generic_quotient.v | |
| parent | 14291b88255b7a1a110c21dec5a3754f25ec8881 (diff) | |
| parent | 37a49513f22a3f792a1ac3241962a7d17455f7e5 (diff) | |
Merge pull request #504 from pi8027/selectors
Revise proofs in ssreflect/*.v
Diffstat (limited to 'mathcomp/ssreflect/generic_quotient.v')
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 4eeada9..5ec4037 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -482,7 +482,7 @@ Lemma equiv_sym : symmetric e. Proof. by case: e => [] ? []. Qed. Lemma equiv_trans : transitive e. Proof. by case: e => [] ? []. Qed. Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T'). -Proof. by move=> x y z; move/eqP->; move/eqP->. Qed. +Proof. by move=> x y z /eqP -> /eqP ->. Qed. Lemma equiv_ltrans: left_transitive e. Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed. @@ -598,8 +598,7 @@ Definition pi := locked (fun x => EquivQuotient (canon_id x)). Lemma ereprK : cancel erepr pi. Proof. -unlock pi; case=> x hx; move/eqP:(hx)=> hx'. -exact: (@val_inj _ _ [subType for erepr]). +by unlock pi; case=> x hx; apply/(@val_inj _ _ [subType for erepr])/eqP. Qed. Local Notation encDE := (encModRelE encD). @@ -629,9 +628,7 @@ exact/pi_CD. Qed. Lemma equivQTP : cancel (CD \o erepr) (pi \o DC). -Proof. -by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP. -Qed. +Proof. by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP. Qed. Local Notation qT := (type_of (Phantom (rel D) encD)). Definition quotClass := QuotClass equivQTP. |