How to prove well-founded recursion

Stream: Is there code for X?

[Atticus Kuhn]

I was trying to program the Fubini Numbers in Lean (see https://oeis.org/A000670 ) with the following code

open_locale big_operators
variables (n m i j k : ℕ)
theorem sub_less (n k :ℕ ) :n - k < n + 1 := begin
 sorry,
end
def ot:  ℕ → ℕ
  | 0 := 1
  | (n + 1) :=
  have lt: n - k < n + 1 := sub_less (n) k,
  ∑  k in finset.range (n+1),  (nat.choose (n+1) (k+1))*ot(n-k)

and I received the following error

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
default_dec_tac failed
state:
k : ℕ,
ot : ℕ → ℕ,
n : ℕ,
lt : n - k < n + 1,
k : ℕ
⊢ n - k < n + 1

How can I tell Lean to use the assumption lt or how can I convince Lean that the Fubini Numbers are well defined. I would appreciate any help or assistance.

[Thomas Browning]

Another option is to define Fubini numbers directly in terms of Stirling numbers.
But if you want to define Fubini numbers recursively, then I suggest you take a look at the definition of docs#catalan.

[Atticus Kuhn]

I figured out the problem. Here is the correct code

theorem sub_less (n k :ℕ ) :n - k < n.succ := begin
--  ring_nf,
 sorry,
  -- exact  nat.sub_lt  npos (nat.succ_pos k),
end

def ot:  ℕ → ℕ
  | 0 := 1
  | (nat.succ n) :=
               ∑  k :  finset.range (n+1),
                have n - k < n.succ, from (sub_less n k),
                (nat.choose (n+1) (k+1))*ot(n-k)