U64int.lev: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as U64int
Lines 659-661 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&start_line=659&end_line=661

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

# le(x, y) on WU.U64 is is_le on the values
def lev(+x: WU.U64, +y: WU.U64, +nx: Nat, +ny: Nat, +hx: {v(x) == nx : Nat}, +hy: {v(y) == ny : Nat}) -> {G.le(~WU.U64, ~I.u64_is, x, y) == Nat.is_le(nx, ny) : Bool}:
  Equal.trans(Bool, Bool.not(I.u64_is(NM.Lt{y, x})), Bool.not(Nat.is_lt(ny, nx)), Nat.is_le(nx, ny), Equal.cong(Bool, Bool, t => Bool.not(t), I.u64_is(NM.Lt{y, x}), Nat.is_lt(ny, nx), ltv(y, x, ny, nx, hy, hx)), nle(ny, nx, Nat.is_lt(ny, nx), {==}))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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.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.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/math/typed/u64int.bend&name=ltv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=nle
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_is
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Test
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64