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
Iris
Iris
Commits
5874f41e
Commit
5874f41e
authored
Mar 09, 2017
by
Ralf Jung
Browse files
show frac_valid'
parent
1c14ae6f
Pipeline
#4015
passed with stage
in 2 minutes and 58 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/frac.v
View file @
5874f41e
...
...
@@ -48,5 +48,8 @@ Proof.
eapply
Qclt_not_eq
;
first
done
.
by
apply
(
inj
(
Qcplus
q
)).
Qed
.
Lemma
frac_op'
:
∀
(
p
q
:
Qp
),
(
p
⋅
q
)
=
(
p
+
q
)%
Qp
.
Lemma
frac_op'
(
q
p
:
Qp
)
:
(
p
⋅
q
)
=
(
p
+
q
)%
Qp
.
Proof
.
done
.
Qed
.
Lemma
frac_valid'
(
p
:
Qp
)
:
✓
p
↔
(
p
≤
1
%
Qp
)%
Qc
.
Proof
.
done
.
Qed
.
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