Fin2.IsLT.h

theorem Fin2.IsLT.h : ∀ {m n : ℕ} [self : Fin2.IsLT m n], m < n

This theorem states that for any two natural numbers `m` and `n`, given the condition that `m` is less than `n` via the `Fin2.IsLT` field, it proves that `m` is indeed less than `n`. Essentially, it verifies the truth of the `Fin2.IsLT` field, which asserts a less-than relationship between two natural numbers.

More concisely: Given `m` and `n` as natural numbers with `m < n`, the theorem verifies that `m` is less than `n`.