def leb_succ

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

import Base

632# a <= b  ->  a <= 1 + b
633def leb_succ(a: Nat, b: Nat, e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, 1n+b) : Bool}:
634  match a b:
635    case 0n _:
636      {==}
637    case 1n+p 0n:
638      %e : BD(_, Unit, {True{} == leb(1n+p, 1n) : Bool})
639      Unit{}
640    case 1n+p 1n+q:
641      leb_succ(p, q, e)