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
  h : forall n : nat, P (max - n)
  n : nat
  n0 : ~ (Z.of_nat max <= Z.of_nat n)%Z
  cstr : (0 <= Z.of_nat n)%Z
  cstr0 : (0 <= Z.of_nat max)%Z
  z1 : Z
  H1 : (0 < Z.of_nat max - Z.of_nat n)%Z /\
       z1 = (Z.of_nat max - Z.of_nat n)%Z \/
       (Z.of_nat max - Z.of_nat n <= 0)%Z /\ z1 = 0%Z
  z2 : Z
  H2 : (0 < Z.of_nat max - z1)%Z /\ z2 = (Z.of_nat max - z1)%Z \/
       (Z.of_nat max - z1 <= 0)%Z /\ z2 = 0%Z
  ============================
   (z2 = Z.of_nat n)


DEBUG:Going to execute:
idtac
DEBUG LTAC Evaluated term: false
Level 2: Zify.zify_convert_to_euclidean_division_equations_flag
 has value 
false