def sp.mod16

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:166

import Base

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