def le_add_l

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/arith.bend:50

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

50# b <= a + b
51def le_add_l(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}:
52  le_subst(b, Nat.add(b, a), Nat.add(a, b), N.add_comm(b, a), N.le_add_right(b, a))