gistfile1.hs

 data _≤_ : ℕ → ℕ → Set where
    z≤z : zero ≤ zero
    s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
    z≤s : {n : ℕ} → zero ≤ suc n

  _<=_ : (n : ℕ) → (m : ℕ) → n ≤ m
  _<=_ zero zero       = z≤z
  _<=_ (suc n) (suc m) = s≤s (n <= m)  
  _<=_ zero (suc n)    = z≤s
  _<=_ (suc _) zero = {!?0 : suc .n ≤ zero!}