rw [Nat.lt_add_one_iff, Finset.le_fold_max]
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < Finset.fold max 0 (fun p_1 => toFunction p_1 (len p)) (ofLen (len p)) + 1
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ 0 ∨ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)