def un.lts
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOFimport Base
2215def un.lts(x: Nat, y: Nat) -> {Nat.is_lt(x, 1n+y) == Nat.is_le(x, y) : Bool}:
2216 Equal.sym(Bool, Nat.is_le(1n+x, 1n+y), Nat.is_lt(x, 1n+y), un.le_succ(x, 1n+y))
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOFimport Base
2215def un.lts(x: Nat, y: Nat) -> {Nat.is_lt(x, 1n+y) == Nat.is_le(x, y) : Bool}:
2216 Equal.sym(Bool, Nat.is_le(1n+x, 1n+y), Nat.is_lt(x, 1n+y), un.le_succ(x, 1n+y))