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
f5082bd5
Commit
f5082bd5
authored
Oct 04, 2016
by
Zhen Zhang
Browse files
tweak the Qp lemmas
parent
1a18f2ff
Changes
2
Hide whitespace changes
Inline
Side-by-side
algebra/frac.v
View file @
f5082bd5
...
...
@@ -35,6 +35,3 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp.
Proof
.
move
=>
y
/
Qcle_not_lt
[]
/=.
by
rewrite
-{
1
}(
Qcplus_0_r
1
)
-
Qcplus_lt_mono_l
.
Qed
.
Lemma
invalid_plus_q
:
∀
(
q
:
Qp
),
¬
✓
(
1
+
q
)%
Qp
.
Proof
.
intros
q
H
.
by
apply
(
Qp_ge_1
q
).
Qed
.
prelude/numbers.v
View file @
f5082bd5
...
...
@@ -567,9 +567,12 @@ Proof.
apply
Qp_eq
;
simpl
.
ring
.
Qed
.
Lemma
Qp_ge_1
(
q
:
Qp
)
:
¬
((
1
+
q
)%
Qp
≤
1
%
Qp
)%
Qc
.
Lemma
Qp_
not_plus_q_
ge_1
(
q
:
Qp
)
:
¬
((
1
+
q
)%
Qp
≤
1
%
Qp
)%
Qc
.
Proof
.
intros
Hle
.
apply
(
Qcplus_le_mono_l
q
0
1
)
in
Hle
.
apply
Qcle_ngt
in
Hle
.
by
destruct
q
.
apply
Qcle_ngt
in
Hle
.
apply
Hle
,
Qp_prf
.
Qed
.
Lemma
Qp_ge_0
(
q
:
Qp
)
:
(
0
≤
q
)%
Qc
.
Proof
.
apply
Qclt_le_weak
,
Qp_prf
.
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