def sc_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32alg.bend:39

import Base

39def sc_zero(+n: Nat) -> {sc(n, 0n) == 0n : Nat}:
40  match n:
41    case 0n:
42      {==}
43    case 1n+p:
44      %Equal.sym(Nat, sc(p, 0n), 0n, sc_zero(p)) : {Nat.double(_) == 0n : Nat}
45      {==}