Goal:
  
  max : nat
  P : nat -> Prop
  hmax : forall n : nat, n >= max -> P n
  hS : forall n : nat, n < max -> P (S n) -> P n
  ============================
   (max - 0 >= max)


DEBUG:Going to execute:
lia
DEBUG LTAC Evaluated term: (forall n : nat, P (max - n))
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: hmax