~/jendhub

def tr.add_zero

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

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base

889def tr.add_zero(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
890  match a:
891    case 0n:
892      {==}
893    case 1n+q:
894      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(q, 0n), q, tr.add_zero(q))

Uses (3)

Used by (1)