Goal:
  
  P : nat -> Prop
  h : forall n : nat, (forall m : nat, m < n -> P m) -> P n
  n : nat
  IHn : forall m : nat, m < n -> P m
  m : nat
  n0 : Z.of_nat n <> Z.of_nat m
  hh : (Z.of_nat m < Z.of_nat n + 1)%Z
  cstr : (0 <= Z.of_nat m)%Z
  cstr0 : (0 <= Z.of_nat n)%Z
  ============================
   (Z.of_nat m < Z.of_nat n)%Z


DEBUG:Going to execute:
constr:(false)