Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
576e6a3a
Commit
576e6a3a
authored
Aug 29, 2019
by
Robbert Krebbers
Browse files
Tweak names in proof.
parent
c85f2e0d
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/big_op.v
View file @
576e6a3a
...
...
@@ -128,11 +128,11 @@ Section list.
Global
Instance
big_opL_ne
n
:
Proper
(
pointwise_relation
_
(
pointwise_relation
_
(
dist
n
))
==>
eq
==>
dist
n
)
(
big_opL
o
(
A
:
=
A
)).
Proof
.
intros
f
g
Hf
m
?
<-.
apply
big_opL_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Proof
.
intros
f
f'
Hf
l
?
<-.
apply
big_opL_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Global
Instance
big_opL_proper'
:
Proper
(
pointwise_relation
_
(
pointwise_relation
_
(
≡
))
==>
eq
==>
(
≡
))
(
big_opL
o
(
A
:
=
A
)).
Proof
.
intros
f
g
Hf
m
?
<-.
apply
big_opL_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Proof
.
intros
f
f'
Hf
l
?
<-.
apply
big_opL_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Lemma
big_opL_consZ_l
(
f
:
Z
→
A
→
M
)
x
l
:
([^
o
list
]
k
↦
y
∈
x
::
l
,
f
k
y
)
=
f
0
x
`
o
`
[^
o
list
]
k
↦
y
∈
l
,
f
(
1
+
k
)%
Z
y
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment