def brA_eq

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

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

117def brA_eq(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.is_eq(C.shift(32n, U), Nat.mul(Q, Q)) == Nat.is_eq(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)) : Bool}:
118  Equal.trans(Bool, Nat.is_eq(C.shift(32n, U), Nat.mul(Q, Q)), Nat.is_eq(C.shift(64n, n), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.is_eq(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), eqsh(C.shift(64n, n), Nat.mul(Q, Q), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U), identN(s, rr, n, Q, U, D, hn, hD, hc)), QW.eq_comm(C.shift(64n, n), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))))