apply Nat.ne_of_lt
p : LoopProgram
h : toFunction p = diagonal
⊢ False
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a = ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

case b
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ