def hlf_succ_le

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

import Base

71def hlf_succ_le(+q: Nat) -> {Nat.is_le(hlf(1n+q), q) == True{} : Bool}:
72  match q:
73    case 0n:
74      {==}
75    case 1n+r:
76      hlf_le(r)