def b_s2

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

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/lib/logic.bend as L
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/natural/arith.bend as NR

166# S2^2 + (c - 2) == N + (D - c) for c < D
167def b_s2(+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.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)) == Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) : Nat}:
168  +eD = N.sub_add(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.lt_le(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx, hb))
169  +e1 = L.subst(Nat, z => {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), z) : Nat}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), b_s1(n, S2, Dx, hnd))
170  +e2 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), NA.add_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), e1, NA.add_swap(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))))
171  +e3 = NR.add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e2)
172  Equal.trans(Nat, Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.trans(Nat, Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), Nat.mul(1n+S2, 1n+S2), NA.add_comm(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Equal.sym(Nat, Nat.mul(1n+S2, 1n+S2), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), sq1_eq(S2))), e3)