def le_add_right

bendtorch-core@0.1.0.0 · src/storage/api.bend:159

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

159def le_add_right(+c: Nat, +x: Nat) -> {Nat.is_le(c, Nat.add(c, x)) == True{} : Bool}:
160  match c:
161    case 0n:
162      Arith.le_zero(x)
163    case 1n+r:
164      le_add_right(r, x)