def bxor_le
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:198
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as Xbits
import Base
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/lib/arith.bend as AR
198def bxor_le(+a: Nat, +b: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {Nat.is_le(S.bxor(a, b), 1n) == True{} : Bool}:
199 match a:
200 case 0n:
201 hb
202 case 1n+q:
203 AR.sub_le2(1n, b)