def low_addlow

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/montnat.bend:14

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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

14def low_addlow(+kk: Nat, +a: Nat, +b: Nat) -> {C.low(kk, Nat.add(a, C.low(kk, b))) == C.low(kk, Nat.add(a, b)) : Nat}:
15  Equal.sym(Nat, C.low(kk, Nat.add(a, b)), C.low(kk, Nat.add(a, C.low(kk, b))), Equal.trans(Nat, C.low(kk, Nat.add(a, b)), C.low(kk, Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b))))), C.low(kk, Nat.add(a, C.low(kk, b))), Equal.cong(Nat, Nat, z => C.low(kk, Nat.add(a, z)), b, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b))), WW.low_high(kk, b)), Equal.trans(Nat, C.low(kk, Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b))))), C.low(kk, Nat.add(Nat.add(a, C.low(kk, b)), C.shift(kk, C.high(kk, b)))), C.low(kk, Nat.add(a, C.low(kk, b))), Equal.cong(Nat, Nat, z => C.low(kk, z), Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b)))), Nat.add(Nat.add(a, C.low(kk, b)), C.shift(kk, C.high(kk, b))), Equal.sym(Nat, Nat.add(Nat.add(a, C.low(kk, b)), C.shift(kk, C.high(kk, b))), Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b)))), NA.add_assoc(a, C.low(kk, b), C.shift(kk, C.high(kk, b))))), WW.low_add_shift(kk, Nat.add(a, C.low(kk, b)), C.high(kk, b)))))