def bn_bo

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

import Base
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

56# the position of m + 1 is 1 + the value of m
57def bn_bo(+b: Bool, +c: Bool, +one: Nat, +h1: {one == 1n : Nat}, +e: {SF.bn(b) == WD.bo(c, one) : Nat}) -> {WD.bo(b, one) == WD.bo(c, one) : Nat}:
58  match b c:
59    case True{} True{}:
60      {==}
61    case False{} False{}:
62      {==}
63    case True{} False{}:
64      Empty.absurd({one == 0n : Nat}, N.succ_zero(0n, e))
65    case False{} True{}:
66      Empty.absurd({0n == one : Nat}, N.zero_succ(0n, Equal.trans(Nat, 0n, one, 1n, e, h1)))