Eqf.w_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as Eqf
Lines 21-24 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend&start_line=21&end_line=24

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G

def w_eq(+pp: Nat, +A: Nat, +B: Nat, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}) -> {Nat.add(pw(pp, A, B), B) == Nat.add(A, 1n+pp) : Nat}:
  +P = {1n+pp : Nat}
  +le = N.le_trans(B, P, Nat.add(A, P), N.lt_le(B, P, hB), G.le_add_l(A, P))
  Equal.trans(Nat, Nat.add(pw(pp, A, B), B), Nat.add(B, pw(pp, A, B)), Nat.add(A, P), NA.add_comm(pw(pp, A, B), B), N.sub_add(Nat.add(A, P), B, le))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=le_add_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_add