def w_ne

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

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/math/natural/arith.bend as NR

54def w_ne(+pp: Nat, +A: Nat, +B: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +h: {Nat.mod(pw(pp, A, B), 1n+pp) == 0n : Nat}) -> {A == B : Nat}:
55  +P = {1n+pp : Nat}
56  +w = pw(pp, A, B)
57  +q = Nat.div(w, P)
58  +e1 = NR.dm_eq(pp, w)
59  +e2 = Equal.trans(Nat, w, Nat.add(Nat.mul(q, P), Nat.mod(w, P)), Nat.add(Nat.mul(q, P), 0n), e1, Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(q, P), z), Nat.mod(w, P), 0n, h))
60  +e3 = Equal.trans(Nat, w, Nat.add(Nat.mul(q, P), 0n), Nat.mul(q, P), e2, N.add_zero(Nat.mul(q, P)))
61  +e4 = Equal.trans(Nat, Nat.add(Nat.mul(q, P), B), Nat.add(w, B), Nat.add(A, P), Equal.cong(Nat, Nat, z => Nat.add(z, B), Nat.mul(q, P), w, Equal.sym(Nat, w, Nat.mul(q, P), e3)), w_eq(pp, A, B, hB))
62  q_one(pp, A, B, q, hA, hB, e4)