# How to get the power of 2 working

Trying to prove: All even numbers > 0 is the product of an odd number and a power of 2 ?
tried on NAT numbers and Z numbers cannot figure out how to prove it. And as well
for m > 0: :2^m = 2*2(m-1)
Is it because i am an amateur ?

You may have a look at this development for your first point. By the way, why restricting to “even numbers”?
For the second:

``````Require Import PeanoNat.
Goal forall m, m > 0 -> 2^m = 2*2^(m-1).
Proof.
intros m Hgt; destruct m.
- inversion Hgt.
- now simpl; rewrite Nat.sub_0_r.
Qed.
``````

What kind of problem did you encounter? What part did stuck?
Do you need hints or complete solution is okay too?

For hints:

1. prove that

``````even n -> exists k, n = k * 2
``````
2. Use lt_wf_ind induction and even_odd_dec:

``````Theorem thm n (H: n <> 0): exists i k, odd k /\ n = k * 2^i.
Proof.
induction n using lt_wf_ind.
destruct (even_odd_dec n).
. . .
Qed.``````

Thank youI am looking into the hints. When to use Nat and when to use Z numbers ?.

Thank you for the response. I will more into this response.
----- Original meddelelse -----

Use nat when proving about natural numbers and use Z when proving about integers, as far as I understand.

2 Likes

Note for this kind of statement:

the best is certainly to write:

``````forall m : nat, 2 ^ (S m) = 2 * 2 ^ m
``````

avoiding the use of `_ - _`. This one is solved by `reflexivity`.