def un.not_lt_add

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

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

import Base

240# A + B < A never holds
241def un.not_lt_add(a: Nat, b: Nat) -> {Nat.is_lt(Nat.add(a, b), a) == False{} : Bool}:
242  match a:
243    case 0n:
244      match b:
245        case 0n:
246          {==}
247        case 1n+q:
248          {==}
249    case 1n+p:
250      un.not_lt_add(p, b)

Uses (4)

Used by (2)