def le_add_l
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:101
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as Poly
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
101def le_add_l(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}:
102 %NA.add_comm(b, a) : {Nat.is_le(b, _) == True{} : Bool}
103 N.le_add_right(b, a)