Commit 2026-05-10 01:42 1bfec08c

View on Github →

chore(Data/Int/Init): generalize le_induction from Prop to Sort* + def lemmas (#37171)

  • Generallise le_induction from Prop to Sort* and rename to leInduction
  • Add a few lemmas
  • Simplify proofs using lia
  • Move inductionOn'_add_one Zulip 💬

Estimated changes

deleted theorem Int.inductionOn'_add_one
modified theorem Int.inductionOn'_sub_one
added theorem Int.leInduction_base