def iz_sc

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

141def iz_sc(+k: Nat, +x: Nat) -> {Nat.is_eq(WD.sc(k, x), 0n) == Nat.is_eq(x, 0n) : Bool}:
142  match k:
143    case 0n:
144      {==}
145    case 1n+ +q:
146      Equal.trans(Bool, Nat.is_eq(Nat.double(WD.sc(q, x)), 0n), Nat.is_eq(WD.sc(q, x), 0n), Nat.is_eq(x, 0n), iz_dbl(WD.sc(q, x)), iz_sc(q, x))