add_zero.bend source

add_zero.bend on the hub · documented module

# Adding zero changes nothing: one proof, published to test the hubimport Baselaw add_zero:  for x: Nat  {Nat.add(x, 0n) == x : Nat}def add_zero(x):  match x:    case 0n:      {==}    case 1n+p:      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}      {==}