Skip to content

Delete "SOLUTION" comment in C02 S03 - #413

Open
SnirBroshi wants to merge 1 commit into
avigad:masterfrom
SnirBroshi:patch-3
Open

SnirBroshi wants to merge 1 commit into
avigad:masterfrom
SnirBroshi:patch-3

Conversation

@SnirBroshi

@SnirBroshi SnirBroshi commented Aug 30, 2026

Copy link
Copy Markdown

This comment appears in C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean next to the SOLUTIONS: section on line 320 that follows the TEXT: section:

-- SOLUTION.
example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  apply sub_le_sub_left
  exact exp_le_exp.mpr h

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant