~/jendhub

def jam_z

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addp.bend:25

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend as F64addp
import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

25def jam_z(+h: Nat) -> {SW.jam(h, 0n) == h : Nat}:
26  SH.jam0_m(h, Nat.mod(h, 2n), {==}, NR.dm_lt(1n, h))

Uses (5)

Used by (1)