law add_zero_right

bend-prot@0.1.0.0 · LAWS.bend:322

import bend-prot@0.1.0.0/LAWS.bend as LAWS
import Base

322# Adding zero on the right changes nothing (induction seed for comm).
323law add_zero_right:
324  for b: Nat
325  {Nat.add(b, 0n) == b : Nat}

Uses (2)

Used by (1)