IdrisDoc: Data.Nat

Data.Nat

diff : Nat -> Nat -> Nat
lteCongMult : (k : Nat) -> LTE m n -> LTE (m * k) (n * k)
lteCongPlus : (k : Nat) -> LTE m n -> LTE (m + k) (n + k)
lteMult : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 * m2) (n1 * n2)
ltePlus : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 + m2) (n1 + n2)