In L11L03 (and I'm pretty sure in some previous level(s) as well), we essentially derive abs_sub:
|
have f2 : |a m| = |(a m - a N) + a N| := by ring_nf |
|
have f3 : |(a m - a N) + a N| ≤ |a m - a N| + |a N| := by apply abs_add |
It would be nice to have access to that theorem -- one could imagine its derivation being a (rather simple) problemset exercise
In L11L03 (and I'm pretty sure in some previous level(s) as well), we essentially derive
abs_sub:RealAnalysisGame/Game/Levels/L11Levels/L03_IsBddOfCauchy.lean
Lines 67 to 68 in 5584aa2
It would be nice to have access to that theorem -- one could imagine its derivation being a (rather simple) problemset exercise