def identN

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

79# N + q^2 == S0^2 + u 2^32, with N = nh 2^64
80def identN(+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.add(C.shift(64n, n), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}:
81  Equal.trans(Nat, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(Q, Q)), C.shift(64n, n), C.shift(32n, C.shift(32n, n)), nn(n)), ident(s, rr, n, Q, U, D, hn, hD, hc))