def mz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:34

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

34def mz(+p: Nat) -> {WD.uw(p, WD.mask(p, 0n)) == 0n : Nat}:
35  match p:
36    case 0n:
37      {==}
38    case 1n+ +q:
39      Equal.cong(Nat, Nat, t => Nat.double(t), WD.uw(q, WD.mask(q, 0n)), 0n, mz(q))