375theorem lt_irrefl (n : LogicNat) : ¬ n < n := by
proof body
Term-mode proof.
376 rintro ⟨k, hk⟩ 377 -- n + succ k = n. Apply toNat: toNat n + toNat (succ k) = toNat n on Nat. 378 have := congrArg toNat hk 379 rw [toNat_add, toNat_succ] at this 380 -- this : toNat n + Nat.succ (toNat k) = toNat n 381 omega 382
used by (11)
From the project-wide theorem graph. These declarations reference this one in their body.