~/jendhub

def internal_lt_one_succ

bend-mathlib@0.8.1.0 · nat.bend:3500

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

3500def internal_lt_one_succ(y: Nat, h: lt(y, 1n)) -> {Bool.or(Nat.is_eq(1n+y, 0n), Nat.is_eq(1n+y, 1n)) == True{} : Bool}:
3501  match y:
3502    case 0n:
3503      {==}
3504    case 1n+z:
3505      Empty.absurd({Bool.or(Nat.is_eq(2n+z, 0n), Nat.is_eq(2n+z, 1n)) == True{} : Bool}, lt_zero(z)(h))

Uses (7)

Used by (1)