order of inputs to function

Stream: general

[Kevin Buzzard]

Sorry if this is already covered somewhere. What should the order of the inputs be in a definition such as

lemma nth_root_pow_left {x : ℝ} {m n : ℕ} (Hm : 0 < m) (Hx : 0 < x) :
(nth_root x m) ^ (m * n) = x ^ n :=

? I'm writing a little library about n'th roots and I've realised that I'm just putting the reals and nats and positivity facts in random and inconsistent orders.

[Kenny Lau]

x before m, so x before m