Are there Isabelle/Isar proof strategies to prove lemmas about non-inductive definitions?

Question

I have Isabelle theory with non-inductive definition (I would like to model algorithms avoiding induction as usually is done by industrial developers) and lemma that is stated for this definition:

theory Maximum
  imports (* Main *)
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

lemma spec_1:
  fixes a :: nat and b :: nat
  assumes "a > b"
  shows "two_integer_max_case_def a b = a"
  apply (induction b)
  apply (induction a)
  apply simp_all
  done

end

Current proof state has generated 3 goals all of them are connected with induction (direct application of simp fails with Failed to apply proof method):

proof (prove)
goal (3 subgoals):
 1. two_integer_max_case_def 0 0 = 0
 2. ⋀a. two_integer_max_case_def a 0 = a ⟹
         two_integer_max_case_def (Suc a) 0 =
         Suc a
 3. ⋀b. two_integer_max_case_def a b = a ⟹
         two_integer_max_case_def a (Suc b) = a

My question is - are there proof methods, strategies that avoid induction and that can be applied in this simple case? Maybe somehow related with simp family of tactics?