def half_go_le

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

import Base

1533# half.go(n, acc) <= n + acc
1534def half_go_le(+n: Nat, +acc: Nat) -> {True{} == leb(half.go(n, acc), Nat.add(n, acc)) : Bool}:
1535  match n:
1536    case 0n:
1537      leb_refl(acc)
1538    case 1n+p:
1539      match p:
1540        case 0n:
1541          leb_succ(acc, acc, leb_refl(acc))
1542        case 1n+q:
1543          %Equal.sym(Nat, 1n+Nat.add(q, acc), Nat.add(q, 1n+acc), add_succ_r(q, acc)) : {True{} == leb(half.go(q, 1n+acc), 1n+_) : Bool}
1544          leb_succ(half.go(q, 1n+acc), Nat.add(q, 1n+acc), half_go_le(q, 1n+acc))