Hint 1 for the have exercise
¶
Try
have h_le : a ≤ a + 1,
Need more
hints
?
Lean at MC 2022
Introduction
1. Logic in Lean - Part 1
2. Logic in Lean - Part 2
3. Infinitely Many Primes
4. Sqrt 2 is irrational
5. Bits & Pieces
Pretty Symbols in Lean
Glossary of Tactics and Lemmas
PDF version
Lean Live Editor
Lean Documentation
Leanprover Community
Quick search