~/jendhub

def le_succ_false

bend-kit-collections@0.1.4.1 · nat_order.bend:149

import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

149def le_succ_false(x: Nat, e: LE(1n+x, x)) -> Empty:
150  match x:
151    case 0n:
152      MBool.false_ne_true()(e)
153    case 1n+p:
154      le_succ_false(p, e)

Uses (4)

Used by (1)