~/jendhub

def sh_y

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

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divn.bend as F64divn
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/width.bend as WW

61# 2^k * y as a product
62def sh_y(+k: Nat, +y: Nat) -> {Nat.mul(C.shift(k, 1n), y) == C.shift(k, y) : Nat}:
63  Equal.trans(Nat, Nat.mul(C.shift(k, 1n), y), C.shift(k, Nat.mul(1n, y)), C.shift(k, y), WW.shift_mul_l(k, 1n, y), Equal.cong(Nat, Nat, z => C.shift(k, z), Nat.mul(1n, y), y, mul1(y)))

Uses (7)

Used by (2)