def le_sh

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divn.bend:65

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

65# le/lt under a common shift
66def le_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_le(C.shift(k, a), C.shift(k, b)) == Nat.is_le(a, b) : Bool}:
67  Equal.cong(Cmp, Bool, c => Cmp.is_le(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))