Add lemmas about Qp and fraction

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

Showing with 7 additions and 0 deletions

theories/numbers.v theories/numbers.v +7 -0

No files found.
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -566,3 +566,10 @@ Proof.
  exists (mk_Qp (q2 - q1 / 2%Z) Hq2'). split; [by rewrite Qp_div_2|].
  apply Qp_eq; simpl. ring.
 Qed.
+
+Lemma Qp_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.
+Qed.