Eqf.q_one: 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 34-52 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=34&end_line=52

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/logic.bend as L
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/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G

# w mod p == 0 gives A == B: the quotient q has w == q p, and q is 1
def q_one(+pp: Nat, +A: Nat, +B: Nat, +q: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +hw: {Nat.add(Nat.mul(q, 1n+pp), B) == Nat.add(A, 1n+pp) : Nat}) -> {A == B : Nat}:
  match q:
    case 0n:
      +P = {1n+pp : Nat}
      +c = L.subst(Nat, z => {Nat.is_le(P, z) == True{} : Bool}, Nat.add(A, P), B, Equal.sym(Nat, B, Nat.add(A, P), hw), G.le_add_l(A, P))
      Empty.absurd({A == B : Nat}, L.true_not_false(Nat.is_lt(B, P), hB, N.le_not_lt(B, P, c)))
    case 1n:
      +P = {1n+pp : Nat}
      +h2 = Equal.trans(Nat, Nat.add(P, B), Nat.add(Nat.mul(1n, P), B), Nat.add(A, P), Equal.cong(Nat, Nat, z => Nat.add(z, B), P, Nat.mul(1n, P), Equal.sym(Nat, Nat.mul(1n, P), P, NA.add_zero(P))), hw)
      NR.add_cancel(P, A, B, Equal.sym(Nat, Nat.add(P, B), Nat.add(P, A), Equal.trans(Nat, Nat.add(P, B), Nat.add(A, P), Nat.add(P, A), h2, NA.add_comm(A, P))))
    case 2n+ +r:
      +P = {1n+pp : Nat}
      +big = Nat.add(P, Nat.add(P, Nat.add(Nat.mul(r, P), B)))
      +h2 = Equal.trans(Nat, big, Nat.add(Nat.mul(2n+r, P), B), Nat.add(A, P), Equal.sym(Nat, Nat.add(Nat.mul(2n+r, P), B), big, Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(P, Nat.mul(r, P))), B), Nat.add(P, Nat.add(Nat.add(P, Nat.mul(r, P)), B)), big, NA.add_assoc(P, Nat.add(P, Nat.mul(r, P)), B), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(P, Nat.mul(r, P)), B), Nat.add(P, Nat.add(Nat.mul(r, P), B)), NA.add_assoc(P, Nat.mul(r, P), B)))), hw)
      +l1 = N.le_add_left(P, Nat.add(P, Nat.add(Nat.mul(r, P), B)), P, N.le_add_right(P, Nat.add(Nat.mul(r, P), B)))
      +l2 = L.subst(Nat, z => {Nat.is_le(Nat.add(P, P), z) == True{} : Bool}, big, Nat.add(A, P), h2, l1)
      +l3 = N.lt_le_trans(Nat.add(A, P), Nat.add(P, P), Nat.add(A, P), N.lt_add_r2(A, P, P, hA), l2)
      Empty.absurd({A == B : Nat}, L.true_not_false(Nat.is_lt(Nat.add(A, P), Nat.add(A, P)), l3, N.lt_irrefl(Nat.add(A, P))))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  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/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  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/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=true_not_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_r2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_irrefl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=add_cancel