diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-06-21 15:02:36 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-06-21 15:03:39 -0400 |
| commit | b8f07f2bb73ea9691c642fd9b32d623bda9b6780 (patch) | |
| tree | 4c07572b09020060c93389bfb807f91bb3d53b08 /src/Util/QUtil.v | |
| parent | ac478e7dc72df91dd51586c345ac4c329f644b14 (diff) | |
src/Demo.v: a 200-line introduction to BaseSystem ideas
Diffstat (limited to 'src/Util/QUtil.v')
| -rw-r--r-- | src/Util/QUtil.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v new file mode 100644 index 000000000..453cad308 --- /dev/null +++ b/src/Util/QUtil.v @@ -0,0 +1,19 @@ +Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround. + +Local Open Scope Z_scope. + +Lemma pow_ceil_mul_nat_nonzero b f + (b_nz:b <> 0) + (f_pos:(0 <= f)%Q) + : forall i, b^Qceiling (f * inject_Z (Z.of_nat i)) <> 0. +Proof. + intros. + eapply Z.pow_nonzero; try omega. + rewrite Zle_Qle. + eapply Qle_trans; [|eapply Qle_ceiling]. + eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial. + cbv; discriminate. + apply (Qle_trans _ (inject_Z 0)); [eapply Qle_refl|]. + rewrite <-Zle_Qle. + eapply Zle_0_nat. +Qed.
\ No newline at end of file |