def le_plus

bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:51

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

51# s <= t + s
52def le_plus(+t: Nat, +s: Nat) -> {Nat.is_le(s, Nat.add(t, s)) == True{} : Bool}:
53  %N.add_comm(s, t) : {Nat.is_le(s, _) == True{} : Bool}
54  N.le_add_right(s, t)