diff options
Diffstat (limited to 'theories/Arith/Div2.v')
| -rw-r--r-- | theories/Arith/Div2.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 016cb85e..a5e45783 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -1,9 +1,11 @@ (************************************************************************) -(* 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) *) (************************************************************************) (** Nota : this file is OBSOLETE, and left only for compatibility. @@ -18,7 +20,7 @@ Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Notation div2 := Nat.div2 (compat "8.4"). +Notation div2 := Nat.div2 (only parsing). (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) @@ -28,7 +30,7 @@ Lemma ind_0_1_SS : P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. intros P H0 H1 H2. - fix 1. + fix ind_0_1_SS 1. destruct n as [|[|n]]. - exact H0. - exact H1. @@ -84,7 +86,7 @@ Qed. (** Properties related to the double ([2n]) *) -Notation double := Nat.double (compat "8.4"). +Notation double := Nat.double (only parsing). Hint Unfold double Nat.double: arith. @@ -103,7 +105,7 @@ Hint Resolve double_S: arith. Lemma even_odd_double n : (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. - revert n. fix 1. destruct n as [|[|n]]. + revert n. fix even_odd_double 1. destruct n as [|[|n]]. - (* n = 0 *) split; split; auto with arith. inversion 1. - (* n = 1 *) |