def from_u
bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:281
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div
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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA
281def from_u(+n: Nat, +w: Word(n)) -> {S.from_nat(n, S.unsigned(n, w)) == w : Word(n)}:
282 %Equal.trans(Nat, Nat.add(S.unsigned(n, w), S.scale_binary(n, 0n)), Nat.add(S.unsigned(n, w), 0n), S.unsigned(n, w), Equal.cong(Nat, Nat, z => Nat.add(S.unsigned(n, w), z), S.scale_binary(n, 0n), 0n, A.sc_zero(n)), N.add_zero(S.unsigned(n, w))) : {S.from_nat(n, _) == w : Word(n)}
283 MA.reconstruct(n, w, 0n)