Goal:
  
  A : Type
  f : A → bool
  g : nat → A
  n : nat
  fg : ∀ x : nat, x < S n → f (g x)
  IHn : (∀ x : nat, x < n → f (g x)) → forallb f (unfold n g)
  x : nat
  lt : BinInt.Z.lt (BinInt.Z.of_nat x) (BinInt.Z.of_nat n)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat n)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat x)
  ============================
   (BinInt.Z.lt (BinInt.Z.of_nat x)
      (BinInt.Z.add (BinInt.Z.of_nat n) (BinNums.Zpos BinNums.xH)))


DEBUG:Going to execute:
constr:(false)