def hlf_le

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32half.bend:60

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

60def hlf_le(+n: Nat) -> {Nat.is_le(hlf(n), n) == True{} : Bool}:
61  match n:
62    case 0n:
63      {==}
64    case 1n+p:
65      match p:
66        case 0n:
67          {==}
68        case 1n+q:
69          N.le_trans(hlf(q), q, 1n+q, hlf_le(q), N.le_succ(q))