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(m1)
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^(m1).
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:

prove that
even n > exists k, n = k * 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
.