390theorem lt_iff_le_and_ne {a b : LogicNat} : a < b ↔ a ≤ b ∧ a ≠ b := by
proof body
Term-mode proof.
391 constructor 392 · rintro ⟨k, hk⟩ 393 refine ⟨⟨succ k, hk⟩, ?_⟩ 394 intro hab 395 rw [hab] at hk 396 -- b + succ k = b means succ k = 0 by additive cancellation; impossible. 397 have := congrArg toNat hk 398 rw [toNat_add, toNat_succ] at this 399 omega 400 · rintro ⟨⟨k, hk⟩, hne⟩ 401 -- a + k = b, a ≠ b, so k ≠ 0; k = succ k' for some k'. 402 cases k with 403 | identity => 404 exfalso 405 apply hne 406 simpa using hk 407 | step k' => exact ⟨k', hk⟩ 408
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.