Theorem: test_pow_le_pow_of_le_one (Ray/Tactic/BoundTests.lean)

State before:
a b c : ℝ
n m : ℕ
a0 : 0 ≤ a
a1 : a ≤ 1
h : n ≤ m
⊢ a ^ m ≤ a ^ n
Tactic:
bound
State after:
no goals