def w_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/eqf.bend:21

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

21def 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}:
22  +P = {1n+pp : Nat}
23  +le = N.le_trans(B, P, Nat.add(A, P), N.lt_le(B, P, hB), G.le_add_l(A, P))
24  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))