U32alg.uniq_gap: 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 64-71 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=64&end_line=71

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

# r1 < 2^n cannot equal r2 + 2^n (1 + q).
def uniq_gap(+n: Nat, +r1: Nat, +r2: Nat, +q: Nat, +h: {Nat.add(r1, sc(n, 0n)) == Nat.add(r2, sc(n, 1n+q)) : Nat}, +b1: {Nat.is_lt(r1, sc(n, 1n)) == True{} : Bool}) -> Empty:
  +e = Equal.trans(Nat, r1, Nat.add(r1, sc(n, 0n)), Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))),
    %Equal.sym(Nat, sc(n, 0n), 0n, sc_zero(n)) : {r1 == Nat.add(r1, _) : Nat}
    Equal.sym(Nat, Nat.add(r1, 0n), r1, N.add_zero(r1)),
    %sc_succ(n, q) : {Nat.add(r1, sc(n, 0n)) == Nat.add(r2, _) : Nat}
    h)
  L.true_false(Equal.trans(Bool, True{}, Nat.is_le(sc(n, 1n), r1), False{}, Equal.sym(Bool, Nat.is_le(sc(n, 1n), r1), True{}, L.subst(Nat, z => {Nat.is_le(sc(n, 1n), z) == True{} : Bool}, Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), r1, Equal.sym(Nat, r1, Nat.add(r2, Nat.add(sc(n, 1n), sc(n, q))), e), le_shift(r2, sc(n, 1n), sc(n, q)))), N.lt_not_le(r1, sc(n, 1n), b1)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=true_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_not_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=le_shift
  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=sc_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=sc_zero