def lt_mn

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

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

524def lt_mn(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +nx: Nat, +hx: {v(x) == nx : Nat}, +h: {Nat.is_lt(nx, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}:
525  lt_m(x, m, mp, hm, L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, nx, v(x), Equal.sym(Nat, v(x), nx, hx), h))