def bends_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:140

import Base

140def bends_zero(+f: Nat) -> {bends(f, 0n) == True{} : Bool}:
141  match f:
142    case 0n:
143      {==}
144    case 1n+g:
145      {==}