WordValue.from_nat_step: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WordValue
Lines 93-99 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&start_line=93&end_line=99

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

def from_nat_step(+p: Nat, +v: Nat, parts: {v == Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)) : Nat} & {Nat.is_le(Nat.mod(v, 2n), 1n) == True{} : Bool}, bound: {Nat.is_lt(v, Nat.mul(2n, Nat.pow(2n, p))) == True{} : Bool}, ih: @+q: Nat -> @hq: {Nat.is_lt(q, Nat.pow(2n, p)) == True{} : Bool} -> {S.unsigned(p, S.from_nat(p, q)) == q : Nat}) -> {S.unsigned(1n+p, S.from_nat(1n+p, v)) == v : Nat}:
  (+eq, le) = parts
  %Equal.sym(Nat, S.unsigned(p, S.from_nat(p, Nat.div(v, 2n))), Nat.div(v, 2n), ih(Nat.div(v, 2n), lt_double(Nat.div(v, 2n), Nat.pow(2n, p), Nat.mod(v, 2n), rescale(p, v, eq, bound)))) : {Nat.add(S.bit_value(Nat.is_eq(Nat.mod(v, 2n), 1n)), Nat.double(_)) == v : Nat}
  %Equal.sym(Nat, S.bit_value(Nat.is_eq(Nat.mod(v, 2n), 1n)), Nat.mod(v, 2n), remainder_bit(Nat.mod(v, 2n), le)) : {Nat.add(_, Nat.double(Nat.div(v, 2n))) == v : Nat}
  %Equal.sym(Nat, v, Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)), eq) : {Nat.add(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n))) == _ : Nat}
  %Equal.sym(Nat, Nat.mul(Nat.div(v, 2n), 2n), Nat.double(Nat.div(v, 2n)), two_times(Nat.div(v, 2n))) : {Nat.add(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n))) == Nat.add(_, Nat.mod(v, 2n)) : Nat}
  A.add_comm(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n)))

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.sym
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&name=lt_double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&name=remainder_bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&name=rescale
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&name=two_times
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned