theorem
proved
wrapper
cumulativeCooling_zero
show as:
view Lean formalization →
formal statement (Lean)
48theorem cumulativeCooling_zero : cumulativeCooling 0 = 0 := by
proof body
One-line wrapper that applies unfold.
49 unfold cumulativeCooling; simp
50