def eq_sh

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:90

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

90def eq_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_eq(C.shift(k, a), C.shift(k, b)) == Nat.is_eq(a, b) : Bool}:
91  Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))