Monus _∸_ is right adjoint to addition _+_ across usual _≤_ preorder

CHANGELOG.md

@@ -2044,6 +2044,10 @@ Other minor changes
   <⇒<′ : m < n → m <′ n
   <′⇒< : m <′ n → m < n
 
+  m≤n⇒[1+m]∸n≡1+[m∸n] : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+  m+n≤p⇒m≤p∸n         : m + n ≤ p → m ≤ p ∸ n
+  m≤p∸n⇒m+n≤p         : n ≤ p → m ≤ p ∸ n → m + n ≤ p
+
   1≤n!    : 1 ≤ n !
   _!≢0    : NonZero (n !)
   _!*_!≢0 : NonZero (m ! * n !)

src/Data/Nat/Properties.agda

@@ -1464,6 +1464,10 @@ n∸n≡0 : ∀ n → n ∸ n ≡ 0
 n∸n≡0 zero    = refl
 n∸n≡0 (suc n) = n∸n≡0 n
 
+m≤n⇒[1+m]∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+m≤n⇒[1+m]∸n≡1+[m∸n] z≤n                                     = refl
+m≤n⇒[1+m]∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] le = refl
+
 ------------------------------------------------------------------------
 -- Properties of _∸_ and pred
 
@@ -1476,6 +1480,15 @@ pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n
 ------------------------------------------------------------------------
 -- Properties of _∸_ and _≤_/_<_
 
+m+n≤p⇒m≤p∸n : ∀ m n p → m + n ≤ p → m ≤ p ∸ n
+m+n≤p⇒m≤p∸n zero    n p       le               = z≤n
+m+n≤p⇒m≤p∸n (suc m) n (suc p) (s≤s le)
+  rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le)
+
+m≤p∸n⇒m+n≤p : ∀ m {n p} (n≤p : n ≤ p) → m ≤ p ∸ n → m + n ≤ p
+m≤p∸n⇒m+n≤p m         z≤n       le rewrite +-identityʳ m = le
+m≤p∸n⇒m+n≤p m {suc n} (s≤s n≤p) le rewrite +-suc m n = s≤s (m≤p∸n⇒m+n≤p m n≤p le)
+
 m∸n≤m : ∀ m n → m ∸ n ≤ m
 m∸n≤m n       zero    = ≤-refl
 m∸n≤m zero    (suc n) = ≤-refl