def lt1_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:613

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

613def lt1_eq(+x: Nat, +h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {Nat.is_eq(x, 0n) == True{} : Bool}:
614  match x:
615    case 0n:
616      {==}
617    case 1n+y:
618      Empty.absurd({Nat.is_eq(1n+y, 0n) == True{} : Bool}, N.lt_zero_absurd(y, h))