Add divisibility properties of exponentials

[Taneb]

No description provided.

[jamesmckinna]

Happy to approve, but I think that each lemma can be improved, as indicated.

[jamesmckinna]

Usual remark applies here: n ≤ o can (and should!) be marked irrelevant, at the (again: usual) cost of expanding the bindings on n and o:

Suggested change

	n≤o⇒m^n∣m^o : ∀ m {n o} → n ≤ o → m ^ n ∣ m ^ o
	n≤o⇒m^n∣m^o m z≤n = 1∣ _
	n≤o⇒m^n∣m^o m (s≤s n≤o) = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m n≤o)
	n≤o⇒m^n∣m^o : ∀ m {n o} → n ≤ o → m ^ n ∣ m ^ o
	n≤o⇒m^n∣m^o m {n = zero} _ = 1∣ _
	n≤o⇒m^n∣m^o m {n = suc _} {o = suc _} n≤o = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m (s≤s⁻¹ n≤o))

[jamesmckinna]

See also #2939 (comment) for a counter view?

[Taneb]

I've made it irrelevant, but just after I pushed, I noticed something further that could be done (assuming #2941) :

n≤o⇒m^n∣m^o : ∀ m {n o} → .(n ≤ o) → m ^ n ∣ m ^ o
n≤o⇒m^n∣m^o m {n} {o} n≤o = divides (m ^ (o ∸ n)) $ begin-equality
  m ^ o               ≡⟨ cong (m ^_) (m∸n+n≡m n≤o) ⟨
  m ^ (o ∸ n + n)     ≡⟨ ^-distribˡ-+-* m (o ∸ n) n ⟩
  m ^ (o ∸ n) * m ^ n ∎
  where open ∣-Reasoning

This has the advantage of making the quotient usefully defined using Data.Nat.Base's operations, rather than a hidden and obscure recursive term. But it's a lot more code for such a small advantage!

[jamesmckinna]

Well...

• let's not assume [ refactor ] Data.Nat.Properties to enforce definitional proof-irrelevance of (in)equational hypotheses where possible #2941 will proceed/progress/land anytime soon!?
• so keep the scope of this PR smaller
• I like the conceptual reduction to Base operations, but agree that the cost-benefit trade-off doesn't immediately indicate a clear win
• ...

All of that said... it's nice to see the commonality between the two proofs, delegating to various instances of distributivity laws. But... for another time, perhaps!?

[jamesmckinna]

So:

Suggested change

	n≤o⇒m^n∣m^o : ∀ m → n ≤ o → m ^ n ∣ m ^ o
	n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o

[jamesmckinna]

This look altogether better, very nicely done.

[jamesmckinna]

💯

[jamesmckinna]

Ah... now I'm home again, i realise I was too hasty: the proof has m/n where better we would have n/m.
Potayto, potahto...