def leb_up

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

import Base

651# a <= b  ->  a <= b + c
652def leb_up(a: Nat, b: Nat, c: Nat, e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, Nat.add(b, c)) : Bool}:
653  match a b:
654    case 0n _:
655      {==}
656    case 1n+p 0n:
657      %e : BD(_, Unit, {True{} == leb(1n+p, Nat.add(0n, c)) : Bool})
658      Unit{}
659    case 1n+p 1n+q:
660      leb_up(p, q, c, e)