PROOF.un.dmu: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 1075-1084 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=1075&end_line=1084

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws

def un.dmu(+b: Nat, +q1: Nat, +r1: Nat, +q2: Nat, +r2: Nat, e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}, h1: {Nat.is_lt(r1, b) == True{} : Bool}, h2: {Nat.is_lt(r2, b) == True{} : Bool}) -> {q1 == q2 : Nat} & {r1 == r2 : Nat}:
  match q1 q2:
    case 0n 0n:
      ({==}, e)
    case 0n 1n+s:
      Empty.absurd({0n == 1n+s : Nat} & {r1 == r2 : Nat}, Laws.nat_succ_add_absurd(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), 1n+b), Nat.add(Nat.sub(b, 1n+r1), 1n+r1), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), 1n+b), Nat.add(Nat.sub(b, 1n+r1), 1n+Nat.add(Nat.mul(0n, b), r1)), Nat.add(Nat.sub(b, 1n+r1), 1n+r1), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), 1n+b), Nat.add(Nat.sub(b, 1n+r1), 1n+Nat.add(Nat.mul(1n+s, b), r2)), Nat.add(Nat.sub(b, 1n+r1), 1n+Nat.add(Nat.mul(0n, b), r1)), ur.r0(Nat.sub(b, 1n+r1), s, b, r2), Equal.cong(Nat, Nat, zz => Nat.add(Nat.sub(b, 1n+r1), 1n+zz), Nat.add(Nat.mul(1n+s, b), r2), Nat.add(Nat.mul(0n, b), r1), Equal.sym(Nat, Nat.add(Nat.mul(0n, b), r1), Nat.add(Nat.mul(1n+s, b), r2), e))), {==}), Laws.nat_lt_witness(r1, b, h1))))
    case 1n+s 1n+t:
      un.dmu.s(s, t, r1, r2, un.dmu(b, s, r1, t, r2, Laws.nat_add_cancel(b, Nat.add(Nat.mul(s, b), r1), Nat.add(Nat.mul(t, b), r2), Equal.trans(Nat, Nat.add(b, Nat.add(Nat.mul(s, b), r1)), Nat.add(Nat.mul(1n+t, b), r2), Nat.add(b, Nat.add(Nat.mul(t, b), r2)), Equal.trans(Nat, Nat.add(b, Nat.add(Nat.mul(s, b), r1)), Nat.add(Nat.mul(1n+s, b), r1), Nat.add(Nat.mul(1n+t, b), r2), ur.r1(b, s, r1), e), ur.r2(t, b, r2))), h1, h2))
    case 1n+s 0n:
      Empty.absurd({1n+s == 0n : Nat} & {r1 == r2 : Nat}, Laws.nat_succ_add_absurd(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), 1n+b), Nat.add(Nat.sub(b, 1n+r2), 1n+r2), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), 1n+b), Nat.add(Nat.sub(b, 1n+r2), 1n+Nat.add(Nat.mul(0n, b), r2)), Nat.add(Nat.sub(b, 1n+r2), 1n+r2), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), 1n+b), Nat.add(Nat.sub(b, 1n+r2), 1n+Nat.add(Nat.mul(1n+s, b), r1)), Nat.add(Nat.sub(b, 1n+r2), 1n+Nat.add(Nat.mul(0n, b), r2)), ur.r0(Nat.sub(b, 1n+r2), s, b, r1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.sub(b, 1n+r2), 1n+zz), Nat.add(Nat.mul(1n+s, b), r1), Nat.add(Nat.mul(0n, b), r2), e)), {==}), Laws.nat_lt_witness(r2, b, h2))))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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_lt
  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.sub
  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-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_witness
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_succ_add_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.dmu.s
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r2