U32alg.w_inj: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as U32alg
Lines 93-95 of bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&start_line=93&end_line=95

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ

def w_inj(+n: Nat, +a: Word(n), +b: Word(n), +e: {uw(n, a) == uw(n, b) : Nat}) -> {a == b : Word(n)}:
  Equal.trans(Word(n), a, S.from_nat(n, uw(n, a)), b, Equal.sym(Word(n), S.from_nat(n, uw(n, a)), a, DQ.reconstruct(n, a)),
    Equal.trans(Word(n), S.from_nat(n, uw(n, a)), S.from_nat(n, uw(n, b)), b, Equal.cong(Nat, Word(n), v => S.from_nat(n, v), uw(n, a), uw(n, b), e), DQ.reconstruct(n, b)))

Uses (8):
  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=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=reconstruct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=uw