RecurrenceProof.fixed_rate_future: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/recurrence_proof.bend as RecurrenceProof
Lines 47-66 of bend-kit-scheduler@0.4.1.0/recurrence_proof.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-scheduler@0.4.1.0/recurrence_proof.bend&start_line=47&end_line=66

import Base
import bend-mathlib@0.7.4.0/nat.bend as N

def fixed_rate_future(+previous: Nat, +completion: Nat, +p: Nat,
  order: Or(N.le(previous, completion), N.le(completion, previous)))
  -> N.lt(completion,
    Nat.add(previous, Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p))):
  match order:
    case Inl{h}:
      %N.add_sub_of_le(previous, completion, h)
        : N.lt(_, Nat.add(previous,
          Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p)))
      N.add_lt_add_left(Nat.sub(completion, previous),
        Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p), previous,
        quotient_future(Nat.sub(completion, previous), p))
    case Inr{+h}:
      %Equal.sym(Nat, Nat.sub(completion, previous), 0n,
        N.sub_eq_zero_of_le(completion, previous, h))
        : N.lt(completion, Nat.add(previous, Nat.mul(1n+Nat.div(_, 1n+p), 1n+p)))
      %Equal.sym(Nat, Nat.add(p, 0n), p, N.add_zero(p))
        : N.lt(completion, Nat.add(previous, 1n+_))
      N.lt_of_le_of_lt(completion, previous, Nat.add(previous, 1n+p), h,
        N.lt_add_of_pos_right(previous, p))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Or
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/recurrence_proof.bend&name=quotient_future
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_sub_of_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt_add_of_pos_right
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt_of_le_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=sub_eq_zero_of_le