def le_succ_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:178

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

178# a + 1 <= b is a < b
179def le_succ_lt(+a: Nat, +b: Nat) -> {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}:
180  match a b:
181    case 0n 0n:
182      {==}
183    case 0n 1n+q:
184      N.zero_le(q)
185    case 1n+p 0n:
186      {==}
187    case 1n+p 1n+q:
188      le_succ_lt(p, q)