case zero

⊢ ascFactorial 0 zero = zero !

case succ
t : ℕ
ht : ascFactorial 0 t = t !
⊢ ascFactorial 0 (succ t) = (succ t)!
k : ℕ
⊢ ascFactorial 0 k = k !
induction' k with t ht
no goals
case succ
t : ℕ
ht : ascFactorial 0 t = t !
⊢ ascFactorial 0 (succ t) = (succ t)!
rw [ascFactorial, ht, zero_add, Nat.factorial_succ]
no goals
case zero

⊢ ascFactorial 0 zero = zero !
rfl