diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /theories/Arith/Div2.v | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'theories/Arith/Div2.v')
-rw-r--r-- | theories/Arith/Div2.v | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 6e5d292f..ca1f39af 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Div2.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Div2.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Lt. Require Import Plus. @@ -173,3 +173,25 @@ Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}. Proof. intros n H. exists (div2 n). auto with arith. Qed. + +(** Doubling before dividing by two brings back to the initial number. *) + +Lemma div2_double : forall n:nat, div2 (2*n) = n. +Proof. + induction n. + simpl; auto. + simpl. + replace (n+S(n+0)) with (S (2*n)). + f_equal; auto. + simpl; auto with arith. +Qed. + +Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n. +Proof. + induction n. + simpl; auto. + simpl. + replace (n+S(n+0)) with (S (2*n)). + f_equal; auto. + simpl; auto with arith. +Qed. |