def lt_half

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:14

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

14# half(n) < m exactly when n < 2m
15def lt_half(+n: Nat, +m: Nat) -> {Nat.is_lt(C.half(n), m) == Nat.is_lt(n, Nat.double(m)) : Bool}:
16  match n m:
17    case 0n 0n:
18      {==}
19    case 0n 1n+mp:
20      {==}
21    case 1n 0n:
22      {==}
23    case 1n 1n+mp:
24      {==}
25    case 2n+ +q 0n:
26      {==}
27    case 2n+ +q 1n+ +mp:
28      lt_half(q, mp)