def le_shift

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32alg.bend:55

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

55# M <= r + (M + s)
56def le_shift(+r: Nat, +m: Nat, +s: Nat) -> {Nat.is_le(m, Nat.add(r, Nat.add(m, s))) == True{} : Bool}:
57  %N.add_comm(Nat.add(m, s), r) : {Nat.is_le(m, _) == True{} : Bool}
58  %Equal.sym(Nat, Nat.add(Nat.add(m, s), r), Nat.add(m, Nat.add(s, r)), N.add_assoc(m, s, r)) : {Nat.is_le(m, _) == True{} : Bool}
59  N.le_add_right(m, Nat.add(s, r))