def iz_dbl

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/canon.bend:134

import Base

134def iz_dbl(+x: Nat) -> {Nat.is_eq(Nat.double(x), 0n) == Nat.is_eq(x, 0n) : Bool}:
135  match x:
136    case 0n:
137      {==}
138    case 1n+q:
139      {==}