def add_succ_nle

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/bits.bend:21

import Base

21# a + (1 + b) <= a is false
22def add_succ_nle(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.add(a, 1n+b), a) == False{} : Bool}:
23  match a:
24    case 0n:
25      {==}
26    case 1n+ +ap:
27      add_succ_nle(ap, b)