feat(algebra/group_power/order): add le_pow (#12436)

Added a new theorem so that library search will find it.



Co-authored-by: seangolinski7 <60711021+seangolinski7@users.noreply.github.com>

src/algebra/group_power/order.lean

@@ -180,6 +180,9 @@ monotone_nat_of_le_succ $ λ n,
 theorem pow_le_pow (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
 pow_mono ha h
 
+theorem le_self_pow (ha : 1 ≤ a) (h : 1 ≤ m) : a ≤ a ^ m :=
+eq.trans_le (pow_one a).symm (pow_le_pow ha h)
+
 lemma strict_mono_pow (h : 1 < a) : strict_mono (λ n : ℕ, a ^ n) :=
 have 0 < a := zero_le_one.trans_lt h,
 strict_mono_nat_of_lt_succ $ λ n, by simpa only [one_mul, pow_succ]