def a24_c
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/ladder.bend:80
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend as Ladder
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
80def a24_c(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +c24: List<&2, U32>, +hv: {K.valo(one, c24) == S.a24(one) : Nat}) -> G.ceq(pp, FS.value(c24), S.a24(one)):
81 G.c_eq(pp, FS.value(c24), S.a24(one), Equal.trans(Nat, FS.value(c24), K.valo(one, c24), S.a24(one), Equal.sym(Nat, K.valo(one, c24), FS.value(c24), K.valo_value(one, h1, c24)), hv))