def eq_ab
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:243
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as F64sqr
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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
243def eq_ab(+q: U32, +u: U32) -> {X.eq(WU.U64{0, u}, X.mul32(q, q)) == Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) : Bool}:
244 Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(SW.value(WU.U64{0, u}), SW.value(X.mul32(q, q))), Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))), WA.eq_value(WU.U64{0, u}, X.mul32(q, q)), Equal.cong(Nat, Bool, z => Nat.is_eq(C.shift(32n, v(u)), z), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))