Add divisibility properties of exponentials (#2940)

* Add divisibility of exponentials

* Make inequality irrelevant

* Simplify m∣n⇒m^o∣n^o definition by reusing ^-distribʳ-*

* Fiddling with variable names

Author: Taneb

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

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 _/_