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.