[ add ] Nat lemmas with _∸_, _⊔_ and _⊓_

Some stuff that I've needed. I have no idea if those belong here in
stdlib.  I don't know if I've put those in the right place, or named
them properly.  Hence the draft and lack of changlog entry.

Author: jkopanski

src/Data/Nat/Properties.agda

@@ -1634,6 +1634,14 @@ m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
   suc ((m + n) ∸ o) ≡⟨ cong suc (+-∸-assoc m o≤n) ⟩
   suc (m + (n ∸ o)) ∎
 
+m∸n+o≡m∸[n∸o] : ∀ {m n o} → n ≤ m → o ≤ n → (m ∸ n) + o ≡ m ∸ (n ∸ o)
+m∸n+o≡m∸[n∸o] {m}     {zero}  {zero}  z≤n       _   = +-identityʳ m
+m∸n+o≡m∸[n∸o] {suc m} {suc n} {zero}  (s≤s n≤m) z≤n = +-identityʳ (m ∸ n)
+m∸n+o≡m∸[n∸o] {suc m} {suc n} {suc o} (s≤s n≤m) (s≤s o≤n)
+  rewrite +-suc (m ∸ n) o
+        | ∸-suc (≤-trans (m∸n≤m n o) n≤m)
+        = cong suc $ m∸n+o≡m∸[n∸o] n≤m o≤n
+
 m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
 m≤n+o⇒m∸n≤o      m  zero    le = le
 m≤n+o⇒m∸n≤o zero    (suc n)  _ = z≤n
@@ -1722,11 +1730,24 @@ even≢odd (suc m) (suc n) eq = even≢odd m n (suc-injective (begin-equality
 ------------------------------------------------------------------------
 -- Properties of _∸_ and _⊓_ and _⊔_
 
+m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n
+m∸n≤m⊔n m n = ≤-trans (m∸n≤m m n) (m≤m⊔n m n)
+
 m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
 m⊓n+n∸m≡n zero    n       = refl
 m⊓n+n∸m≡n (suc m) zero    = refl
 m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
 
+m⊔n∸[m∸n]≡n : ∀ m n → m ⊔ n ∸ (m ∸ n) ≡ n
+m⊔n∸[m∸n]≡n zero    n       rewrite 0∸n≡0 n             = refl
+m⊔n∸[m∸n]≡n (suc m) zero                                = n∸n≡0 m
+m⊔n∸[m∸n]≡n (suc m) (suc n) rewrite ∸-suc (m∸n≤m⊔n m n) = cong suc $ m⊔n∸[m∸n]≡n m n
+
+m⊔n≡m∸n+n : ∀ m n → m ⊔ n ≡ m ∸ n + n
+m⊔n≡m∸n+n zero    n       rewrite 0∸n≡0 n         = refl
+m⊔n≡m∸n+n (suc m) zero    rewrite +-identityʳ m   = refl
+m⊔n≡m∸n+n (suc m) (suc n) rewrite +-suc (m ∸ n) n = cong suc $ m⊔n≡m∸n+n m n
+
 [m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
 [m∸n]⊓[n∸m]≡0 zero zero       = refl
 [m∸n]⊓[n∸m]≡0 zero (suc n)    = refl
@@ -1844,6 +1865,17 @@ m∸n≤∣m-n∣ m n with ≤-total m n
 ∣m-n∣≤m⊔n (suc m) zero    = ≤-refl
 ∣m-n∣≤m⊔n (suc m) (suc n) = m≤n⇒m≤1+n (∣m-n∣≤m⊔n m n)
 
+∣m-n∣≡m⊔n∸m⊓n : ∀ m n → ∣ m - n ∣ ≡ m ⊔ n ∸ m ⊓ n
+∣m-n∣≡m⊔n∸m⊓n m n with ≤-total m n
+... | inj₁ m≤n
+    rewrite m≤n⇒m⊔n≡n m≤n
+          | m≤n⇒m⊓n≡m m≤n
+          = m≤n⇒∣m-n∣≡n∸m m≤n
+... | inj₂ n≤m
+    rewrite m≥n⇒m⊔n≡m n≤m
+          | m≥n⇒m⊓n≡n n≤m
+          = m≤n⇒∣n-m∣≡n∸m n≤m
+
 ∣-∣-identityˡ : LeftIdentity 0 ∣_-_∣
 ∣-∣-identityˡ x = refl