From b8f07f2bb73ea9691c642fd9b32d623bda9b6780 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 21 Jun 2017 15:02:36 -0400 Subject: src/Demo.v: a 200-line introduction to BaseSystem ideas --- src/Util/QUtil.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 src/Util/QUtil.v (limited to 'src/Util/QUtil.v') 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 -- cgit v1.2.3