def dbl_eq0

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:255

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

255def dbl_eq0(+z: Nat) -> {Nat.is_eq(Nat.double(z), 0n) == Nat.is_eq(z, 0n) : Bool}:
256  match z:
257    case 0n:
258      {==}
259    case 1n+ +w:
260      L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, Nat.add(2n, Nat.double(w)), Nat.double(1n+w), Equal.sym(Nat, Nat.double(1n+w), Nat.add(2n, Nat.double(w)), N.double_succ(w)), {==})