~/jendhub

law pow_le_pow_left

bend-mathlib@0.8.1.0 · nat.bend:3324

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

3324# Powers are monotone in the base: a <= b implies a^n <= b^n.
3325law pow_le_pow_left:
3326  for a: Nat
3327  for b: Nat
3328  for h: le(a, b)
3329  for n: Nat
3330  le(Nat.pow(a, n), Nat.pow(b, n))

Uses (4)

Used by (0)

No other definition uses this definition.