~/jendhub

def exp_amt

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

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

59def exp_amt(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(1033n, Nat.sub(63n, j)) == Nat.add(j, 970n) : Nat}:
60  Equal.trans(Nat, Nat.sub(1033n, Nat.sub(63n, j)), Nat.add(970n, j), Nat.add(j, 970n), exp_amt0(j, hj), N.add_comm(970n, j))

Uses (8)

Used by (1)