def r52

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

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

246def r52(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(52n, j), 64n) == True{} : Bool}:
247  +r = Nat.sub(52n, j)
248  +e = Equal.trans(Nat, Nat.add(r, j), Nat.add(j, r), 52n, N.add_comm(r, j), N.sub_add(52n, j, hj))
249  N.le_lt_trans(r, 52n, 64n, L.subst(Nat, z => {Nat.is_le(r, z) == True{} : Bool}, Nat.add(r, j), 52n, e, N.le_add_right(r, j)), {==})