diff --git a/CHANGELOG.md b/CHANGELOG.md
index 598b3e519c..6ef2b7eb43 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -259,6 +259,12 @@ Additions to existing modules
   map : P ⊆ Q → All P xs → All Q xs
   ```
 
+* In `Data.Nat.Divisiblity`:
+  ```agad
+  m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o
+  n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o
+  ```
+
 * In `Data.Nat.Logarithm`
   ```agda
   2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index c5d42a2c90..cba883efab 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -257,6 +257,16 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
     (p + q) * d   ∎
   where open ∣-Reasoning
 
+------------------------------------------------------------------------
+-- Properties of _∣_ and _^_
+
+m∣n⇒m^o∣n^o : ∀ {m n} o → m ∣ n → m ^ o ∣ n ^ o
+m∣n⇒m^o∣n^o o (divides-refl m/n) = divides (m/n ^ o) (^-distribʳ-* o m/n _)
+
+n≤o⇒m^n∣m^o : ∀ m {n o} → .(n ≤ o) → m ^ n ∣ m ^ o
+n≤o⇒m^n∣m^o m {zero} 0≤o = 1∣ _
+n≤o⇒m^n∣m^o m {suc _} {suc _} sn≤so = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m (s≤s⁻¹ sn≤so))
+
 ------------------------------------------------------------------------
 -- Properties of _∣_ and _/_