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
  n : nat
  IHn : P (max - n)
  n0 : ~ max <= n
  ============================
   (P (max - S n))


DEBUG:Going to execute:
<coq-core.plugins.ltac::replace@0> $1 $2 $3 $4
DEBUG LTAC Evaluated term: (S (max - S n))