Std.Data.Nat.Lemmas
source
Strong case analysis on a < b ∨ b ≤ a∨ b ≤ a≤ a
a < b ∨ b ≤ a∨ b ≤ a≤ a
Strong case analysis on a < b ∨ a = b ∨ b < a∨ a = b ∨ b < a∨ b < a
a < b ∨ a = b ∨ b < a∨ a = b ∨ b < a∨ b < a