def zc

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:47

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
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/word.bend as WD

47def zc(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +x: Nat, +c: Bool, +e: {Nat.add(r, C.shift(32n, WD.bo(c, one))) == Nat.add(x, 1n) : Nat}, +hx: {C.fits(32n, x) == True{} : Bool}) -> {SF.bn(Nat.is_eq(r, 0n)) == WD.bo(c, one) : Nat}:
48  match c:
49    case True{}:
50      zc_t(one, h1, r, x, e, hx)
51    case False{}:
52      +er = Equal.trans(Nat, r, Nat.add(r, 0n), 1n+x, Equal.sym(Nat, Nat.add(r, 0n), r, N.add_zero(r)), Equal.trans(Nat, Nat.add(r, 0n), Nat.add(x, 1n), 1n+x, e, N.add_comm(x, 1n)))
53      %Equal.sym(Nat, r, 1n+x, er) : {SF.bn(Nat.is_eq(_, 0n)) == 0n : Nat}
54      {==}