Float.ex: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float
Lines 181-191 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=181&end_line=191

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

# X + r = 2947 for X = j + 2895, r = 52 - j
def ex(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.add(Nat.add(j, 2895n), Nat.sub(52n, j)) == x0() : Nat}:
  +r = Nat.sub(52n, j)
  +e1 = N.sub_add(52n, j, hj)
  +a1 = N.add_assoc(j, 2895n, r)
  +a2 = Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(2895n, r), Nat.add(r, 2895n), N.add_comm(2895n, r))
  +a3 = Equal.sym(Nat, Nat.add(Nat.add(j, r), 2895n), Nat.add(j, Nat.add(r, 2895n)), N.add_assoc(j, r, 2895n))
  +a4 = Equal.cong(Nat, Nat, z => Nat.add(z, 2895n), Nat.add(j, r), 52n, e1)
  Equal.trans(Nat, Nat.add(Nat.add(j, 2895n), r), Nat.add(j, Nat.add(2895n, r)), x0(), a1,
    Equal.trans(Nat, Nat.add(j, Nat.add(2895n, r)), Nat.add(j, Nat.add(r, 2895n)), x0(), a2,
      Equal.trans(Nat, Nat.add(j, Nat.add(r, 2895n)), Nat.add(Nat.add(j, r), 2895n), x0(), a3, a4)))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=x0