~/jendhub

def internal_lt_two

bend-mathlib@0.8.1.0 · nat.bend:3507

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

3507def internal_lt_two(x: Nat, h: lt(x, 2n)) -> {Bool.or(Nat.is_eq(x, 0n), Nat.is_eq(x, 1n)) == True{} : Bool}:
3508  match x:
3509    case 0n:
3510      {==}
3511    case 1n+y:
3512      internal_lt_one_succ(y, h)

Uses (6)

Used by (1)