def un.not_lt_add_l

bend-osdev-u32@0.1.0.0 · PROOF.bend:252

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF

import Base

252def un.not_lt_add_l(+s: Nat, +b: Nat) -> {Nat.is_lt(Nat.add(s, b), b) == False{} : Bool}:
253  %un.add_comm(b, s) : {Nat.is_lt(_, b) == False{} : Bool}
254  un.not_lt_add(b, s)

Uses (6)

Used by (2)