module Data.Nat.Properties.Extra where

open import Data.Nat.Base
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

<-+ : ∀ {m n m' n'} → m ≤ m' → n ≤ n' → m + n ≤ m' + n'
<-+ {zero} {zero} z≤n z≤n = z≤n
<-+ {suc m} (s≤s m<m') x = s≤s (<-+ m<m' x)
<-+ {zero} {suc n} {zero} z≤n (s≤s n<n') = s≤s n<n'
<-+ {zero} {suc n} {suc m'} z≤n (s≤s n<n') = s≤s (<-+ {m' = m'} z≤n (≤-step n<n'))

<-unique : ∀ {i u} (p q : i < u) → p ≡ q
<-unique (s≤s z≤n) (s≤s z≤n) = refl
<-unique (s≤s (s≤s p)) (s≤s (s≤s q)) = sym (cong s≤s (<-unique (s≤s q) (s≤s p)))