Add n≮0 to Data.Nat.Properties

Author: jamesmckinna

CHANGELOG.md

@@ -692,6 +692,7 @@ Other minor changes
 
 * Added new proofs in `Data.Nat.Properties`:
   ```agda
+  n≮0       : n ≮ 0
   n+1+m≢m   : n + suc m ≢ m
   m*n≡0⇒m≡0 : .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
   ```

src/Data/Nat/Properties.agda

@@ -396,6 +396,9 @@ _>?_ = flip _<?_
 ------------------------------------------------------------------------
 -- Other properties of _<_
 
+n≮0 : ∀ {n} → n ≮ 0
+n≮0 ()
+
 n≮n : ∀ n → n ≮ n
 n≮n n = <-irrefl (refl {x = n})