def le_add_right

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:317

import Base

317def le_add_right(+a: Nat, +b: Nat) -> {Nat.is_le(a, Nat.add(a, b)) == True{} : Bool}:
318  match a:
319    case 0n:
320      zero_le(b)
321    case 1n+p:
322      le_add_right(p, b)