def sub_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addp.bend:35

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

35def sub_shift(+d: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.sub(C.shift(d, a), C.shift(d, b)) == C.shift(d, Nat.sub(a, b)) : Nat}:
36  +ea = N.sub_add(a, b, h)
37  Equal.trans(Nat, Nat.sub(C.shift(d, a), C.shift(d, b)), Nat.sub(C.shift(d, Nat.add(b, Nat.sub(a, b))), C.shift(d, b)), C.shift(d, Nat.sub(a, b)), Equal.cong(Nat, Nat, z => Nat.sub(C.shift(d, z), C.shift(d, b)), a, Nat.add(b, Nat.sub(a, b)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, ea)), Equal.trans(Nat, Nat.sub(C.shift(d, Nat.add(b, Nat.sub(a, b))), C.shift(d, b)), Nat.sub(Nat.add(C.shift(d, b), C.shift(d, Nat.sub(a, b))), C.shift(d, b)), C.shift(d, Nat.sub(a, b)), Equal.cong(Nat, Nat, z => Nat.sub(z, C.shift(d, b)), C.shift(d, Nat.add(b, Nat.sub(a, b))), Nat.add(C.shift(d, b), C.shift(d, Nat.sub(a, b))), WW.shift_add(d, b, Nat.sub(a, b))), N.add_sub_cancel(C.shift(d, b), C.shift(d, Nat.sub(a, b)))))