tweak the Qp lemmas

62389c82 · Zhen Zhang · f9c54965 · 62389c82
Commit 62389c82 authored Oct 04, 2016 by Zhen Zhang
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 2 deletions

theories/numbers.v theories/numbers.v +5 -2

No files found.
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -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.