def sp.mod16

import bend-osdev-cbc@0.1.0.0/PROOF.bend as PROOF

import Base

121def sp.mod16(n: Nat) -> {Nat.mod(Nat.add(16n, n), 16n) == Nat.mod(n, 16n) : Nat}:
122  sp.snd_go(n, 15n, 1n, 0n, 0n)

Uses (4)