Fixprime.fuel_ok: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend as Fixprime
Lines 154-167 of bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&start_line=154&end_line=167

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as UA
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3

def fuel_ok(+one: Nat, +h1: {one == 1n : Nat}, +n: U32) -> {Nat.is_le(C.shift(32n, one), Nat.add(1n+v(n), 1n+v(U32.not(n)))) == True{} : Bool}:
  match n:
    case U32{+w}:
      +A = UA.uw(32n, Word.not(32n, w))
      +B = UA.uw(32n, w)
      +S = C.shift(32n, one)
      +e1 = Equal.trans(Nat, S, WD.sc(32n, one), UA.sc(32n, one), W64M.shift_sc(32n, one), {==})
      +eS = Equal.trans(Nat, S, UA.sc(32n, one), Nat.add(1n, Nat.add(A, B)), e1, Equal.sym(Nat, Nat.add(1n, Nat.add(A, B)), UA.sc(32n, one), not_value_one(32n, one, h1, w)))
      +eR = Equal.trans(Nat, Nat.add(1n+B, 1n+A), 1n+Nat.add(B, 1n+A), 2n+Nat.add(A, B), {==}, Equal.cong(Nat, Nat, z => 1n+z, Nat.add(B, 1n+A), 1n+Nat.add(A, B), Equal.trans(Nat, Nat.add(B, 1n+A), 1n+Nat.add(B, A), 1n+Nat.add(A, B), N.add_succ(B, A), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(B, A), Nat.add(A, B), N.add_comm(B, A)))))
      %Equal.sym(Nat, U32.to_nat(U32{w}), B, U3.to_nat_word(w)) : {Nat.is_le(S, Nat.add(1n+_, 1n+U32.to_nat(U32{Word.not(32n, w)}))) == True{} : Bool}
      %Equal.sym(Nat, U32.to_nat(U32{Word.not(32n, w)}), A, U3.to_nat_word(Word.not(32n, w))) : {Nat.is_le(S, Nat.add(1n+B, 1n+_)) == True{} : Bool}
      %Equal.sym(Nat, S, Nat.add(1n, Nat.add(A, B)), eS) : {Nat.is_le(_, Nat.add(1n+B, 1n+A)) == True{} : Bool}
      %Equal.sym(Nat, Nat.add(1n+B, 1n+A), 2n+Nat.add(A, B), eR) : {Nat.is_le(Nat.add(1n, Nat.add(A, B)), _) == True{} : Bool}
      N.le_succ(1n+Nat.add(A, B))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.not
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=to_nat_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=uw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=not_value_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=shift_sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift