# [isabelle] Strong Induction

```Hello,

I'm studying the "A Logical Approach To Discrete Math" and am trying to use
Isabelle with solving a few exercises. I am in the Induction chapter, and I'm
trying to prove:

lemma
fixes x y h :: nat
shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4"

Which would be the equivalent of the first exercise of the chapter which is:

P.n : (\<exists>h,k | 0 <= h /\ 0 <= k: 2*h + 5*k = n) for n>=4

I've searched the web for isabelle strong induction and cases, etc, I've even
tried to read the src/HOL/Tools/inductive.ML but I'm not very proficient in
ML so I really couldn't understand much. So I really have no idea on how
to proceed.

I wrote a proof in my notebook as:

Proved P.0 and proved P.1, then proved that
P.n => P.n+2

But with Isabelle I have no idea how to transpose this. The induct proof
divides in cases 0 and Suc h. So all I have is until now:

lemma
fixes x y h :: nat
shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4"
proof (induct h)
case 0
have "\<exists> x y. 2*x + 5*y = (0::nat) + 4"
apply (rule_tac x = 2 in exI)
by simp
thus ?case .
next
case (Suc n)
and from here I have no idea how to continue.

What I wanted was to:

lemma
fixes x y h :: nat
shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4"
proof (induct h)
case 0
have "\<exists> x y. 2*x + 5*y = (0::nat) + 4"
apply (rule_tac x = 2 in exI)
by simp
thus ?case .
next
case (Suc 0)
(* etc *)
thus ?case .
next
case (Suc (Suc n))
(* prove P.n ==> P (Suc (Suc n)) *)
thus ?case .
qed

Any pointers?