def half_rem

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/bits.bend:37

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

37# n mod 2 <= 1
38def half_rem(+n: Nat) -> {Nat.is_lt(Nat.mod(n, 2n), 2n) == True{} : Bool}:
39  R.dm_lt(1n, n)