Less-Than-or. <. Well-founded relation on Nat.
GHC can solve this for us!
ltProof :: LTProof Nat0 Nat4LESucc LEZero
ltProof :: LTProof Nat2 Nat4LESucc (LESucc (LESucc LEZero))
ltProof :: LTProof Nat3 Nat3......error......
Modulefin-0.3.2Haskell2010
Data.Type.Nat.LT
- 1 type
- 1 class
- 4 values
- Packagefin-0.3.2
- Exports6
- LanguageHaskell2010
- LicenceBSD-3-Clause
- SourceLT.hs
An evidence n < m which is the same as (1 + n le m).
Lemmas
3 declarations\forall n : \mathbb{N}, n < n \to \bot
\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot
\forall n\, m\, p : \mathbb{N}, n < m \to m < p \to n < p