`BookProof.ChapterF8.totalCost_sub_offline` (M d m K₂ k : ℕ) : totalCost M d m K₂ k - offlineCost M d k = onlineCost d m K₂ k

Initializing...

`BookProof.ChapterF8.totalCost_sub_offline` (M d m K₂ k : ℕ) : totalCost M d m K₂ k - offlineCost M d k = onlineCost d m K₂ k · Prove2Me