def leb_up_l

bend-ml-tensor-array@0.1.19.0 · main.bend:643

import Base

643# a <= b  ->  a <= c + b
644def leb_up_l(+a: Nat, +b: Nat, c: Nat, +e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, Nat.add(c, b)) : Bool}:
645  match c:
646    case 0n:
647      e
648    case 1n++c2:
649      leb_succ(a, Nat.add(c2, b), leb_up_l(a, b, c2, e))