def lev

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:658

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

658# le(x, y) on U32 is is_le on the values
659def lev(+x: U32, +y: U32, +nx: Nat, +ny: Nat, +hx: {v(x) == nx : Nat}, +hy: {v(y) == ny : Nat}) -> {G.le(~U32, ~I.u32_is, x, y) == Nat.is_le(nx, ny) : Bool}:
660  Equal.trans(Bool, Bool.not(I.u32_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.u32_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), {==}))