law add_zero_right
import bend-prot@0.1.0.0/LAWS.bend as LAWSimport 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}
import bend-prot@0.1.0.0/LAWS.bend as LAWSimport 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}