diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 33 |
1 files changed, 28 insertions, 5 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index df9b8339..64935ffe 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -1,15 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) Require Export NZAxioms. -Require Import BigNumPrelude. +Require Import ZArith. +Require Import Zpow_facts. Require Import DoubleType. Require Import CyclicAxioms. @@ -139,6 +142,26 @@ rewrite 2 ZnZ.of_Z_correct; auto with zarith. symmetry; apply Zmod_small; auto with zarith. Qed. +Theorem Zbounded_induction : + (forall Q : Z -> Prop, forall b : Z, + Q 0 -> + (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) -> + forall n, 0 <= n -> n < b -> Q n)%Z. +Proof. +intros Q b Q0 QS. +set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)). +assert (H : forall n, 0 <= n -> Q' n). +apply natlike_rec2; unfold Q'. +destruct (Z.le_gt_cases b 0) as [H | H]. now right. left; now split. +intros n H IH. destruct IH as [[IH1 IH2] | IH]. +destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1]. +right; auto with zarith. +left. split; [auto with zarith | now apply (QS n)]. +right; auto with zarith. +unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3]. +assumption. now apply Z.le_ngt in H3. +Qed. + Lemma B_holds : forall n : Z, 0 <= n < wB -> B n. Proof. intros n [H1 H2]. |