def pow_mono

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:474

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2

474def pow_mono(+x: Nat, +y: Nat, +k: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(Nat.pow(x, k), Nat.pow(y, k)) == True{} : Bool}:
475  match k:
476    case 0n:
477      {==}
478    case 1n+ +j:
479      N.le_trans(Nat.mul(x, Nat.pow(x, j)), Nat.mul(y, Nat.pow(x, j)), Nat.mul(y, Nat.pow(y, j)), AR2.mul_le(x, y, Nat.pow(x, j), h), mul_le_r(y, Nat.pow(x, j), Nat.pow(y, j), pow_mono(x, y, j, h)))