def le_add_left

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

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

152def le_add_left(+f: Nat, +k: Nat) -> {Nat.is_le(k, Nat.add(f, k)) == True{} : Bool}:
153  match f:
154    case 0n:
155      le_refl(k)
156    case 1n+q:
157      Arith.le_succ(k, Nat.add(q, k), le_add_left(q, k))