def pred_value

bend-collections-laws-math@1.0.0.0 · proofs/math/random/uint64n.bend:94

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
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/math/typed/w64add.bend as WA

94# n - 1 for a nonzero n
95def pred_value(+n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}) -> {SW.value(X.sub(n, one64())) == m : Nat}:
96  +hle = Equal.trans(Bool, Nat.is_le(1n, SW.value(n)), Nat.is_le(1n, 1n+m), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(1n, z), SW.value(n), 1n+m, hv), N.zero_le(m))
97  Equal.trans(Nat, SW.value(X.sub(n, one64())), Nat.sub(SW.value(n), 1n), m, WA.sub_value(n, one64(), hle),
98    %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {Nat.sub(_, 1n) == m : Nat}
99    N.sub_zero(m))