def leb_add

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

import Base

662# a <= b  and  c <= d  ->  a + c <= b + d
663def leb_add(a: Nat, b: Nat, c: Nat, d: Nat, e1: {True{} == leb(a, b) : Bool}, e2: {True{} == leb(c, d) : Bool}) -> {True{} == leb(Nat.add(a, c), Nat.add(b, d)) : Bool}:
664  match a b:
665    case 0n _:
666      leb_up_l(c, d, b, e2)
667    case 1n+p 0n:
668      %e1 : BD(_, Unit, {True{} == leb(Nat.add(1n+p, c), Nat.add(0n, d)) : Bool})
669      Unit{}
670    case 1n+p 1n+q:
671      leb_add(p, q, c, d, e1, e2)