def b2_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:186

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/f64sqw.bend as QW

186def b2_eq(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}) -> {Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == Nat.is_eq(Nat.mul(S2, S2), C.shift(64n, n)) : Bool}:
187  Equal.trans(Bool, Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.is_eq(Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.is_eq(Nat.mul(S2, S2), C.shift(64n, n)), QW.eq_comm(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), eqsh(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), b_s2(n, S2, Dx, hnd, hb)))