def usq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqk.bend:25

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

25# (s 2^32)^2 + r 2^64 == n 2^64 for s^2 + r == n
26def usq(+s: Nat, +r: Nat, +n: Nat, +hn: {Nat.add(Nat.mul(s, s), r) == n : Nat}) -> {Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, r))) == C.shift(32n, C.shift(32n, n)) : Nat}:
27  Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, r))), Nat.add(C.shift(32n, C.shift(32n, Nat.mul(s, s))), C.shift(32n, C.shift(32n, r))), C.shift(32n, C.shift(32n, n)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.shift(32n, r))), Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.mul(s, s))), AQ.sh_sq(32n, s)), Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, Nat.mul(s, s))), C.shift(32n, C.shift(32n, r))), C.shift(32n, Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), C.shift(32n, C.shift(32n, n)), Equal.sym(Nat, C.shift(32n, Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), Nat.add(C.shift(32n, C.shift(32n, Nat.mul(s, s))), C.shift(32n, C.shift(32n, r))), WW.shift_add(32n, C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), Equal.trans(Nat, C.shift(32n, Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), C.shift(32n, C.shift(32n, Nat.add(Nat.mul(s, s), r))), C.shift(32n, C.shift(32n, n)), Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r)), C.shift(32n, Nat.add(Nat.mul(s, s), r)), Equal.sym(Nat, C.shift(32n, Nat.add(Nat.mul(s, s), r)), Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r)), WW.shift_add(32n, Nat.mul(s, s), r))), Equal.cong(Nat, Nat, z => C.shift(32n, C.shift(32n, z)), Nat.add(Nat.mul(s, s), r), n, hn))))