def lt_two

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/logs.bend:67

import Base

67def lt_two(+bq: Nat) -> {Nat.is_lt(2n+bq, 2n) == False{} : Bool}:
68  match bq:
69    case 0n:
70      {==}
71    case 1n+q:
72      {==}