def ex

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:181

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

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