~/jendhub

def sh_sq

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

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as F64sqa
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

58# shifting a square by j on both factors
59def sh_sq(+j: Nat, +a: Nat) -> {Nat.mul(C.shift(j, a), C.shift(j, a)) == C.shift(j, C.shift(j, Nat.mul(a, a))) : Nat}:
60  Equal.trans(Nat, Nat.mul(C.shift(j, a), C.shift(j, a)), C.shift(j, Nat.mul(a, C.shift(j, a))), C.shift(j, C.shift(j, Nat.mul(a, a))), WW.shift_mul_l(j, a, C.shift(j, a)), Equal.cong(Nat, Nat, z => C.shift(j, z), Nat.mul(a, C.shift(j, a)), C.shift(j, Nat.mul(a, a)), WW.shift_mul_r(j, a, a)))

Uses (7)

Used by (9)