Library Coq.Arith.Div2
Require Import Lt.
Require Import Plus.
Require Import Compare_dec.
Require Import Even.
Open Local Scope nat_scope.
Implicit Type n :
nat.
Here we define n/2 and prove some of its properties
Fixpoint div2 n :
nat :=
match n with
|
O => 0
|
S O => 0
|
S (
S n') =>
S (
div2 n')
end.
Since div2 is recursively defined on 0, 1 and (S (S n)), it is
useful to prove the corresponding induction principle
Lemma ind_0_1_SS :
forall P:
nat ->
Prop,
P 0 ->
P 1 -> (
forall n,
P n ->
P (
S (
S n))) ->
forall n,
P n.
0 <n => n/2 < n
Properties related to the parity
Properties related to the double (2n)
Specializations
Application:
- if n is even then there is a p such that n = 2p
- if n is odd then there is a p such that n = 2p+1
(Immediate: it is
n/2)
Doubling before dividing by two brings back to the initial number.