def low_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/montnat.bend:20

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

20def low_zero(k: Nat) -> {C.low(k, 0n) == 0n : Nat}:
21  match k:
22    case 0n:
23      {==}
24    case 1n+ +p:
25      Equal.cong(Nat, Nat, z => Nat.double(z), C.low(p, 0n), 0n, low_zero(p))