def le_refl

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/num.bend:69

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

69def le_refl(+x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
70  N.le_refl(x)