RecurrenceProof.due_tick: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/recurrence_proof.bend as RecurrenceProof
Lines 75-84 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=75&end_line=84

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

def due_tick(+previous: Nat, +completion: Nat, +p: Nat, +i: Nat,
  h: N.le(previous, completion), hi: N.le(i, Nat.div(Nat.sub(completion, previous), 1n+p)))
  -> N.le(Nat.add(previous, Nat.mul(i, 1n+p)), completion):
  %N.sub_add_cancel(completion, previous, h)
    : N.le(Nat.add(previous, Nat.mul(i, 1n+p)), _)
  %N.add_comm(previous, Nat.sub(completion, previous))
    : N.le(Nat.add(previous, Nat.mul(i, 1n+p)), _)
  N.add_le_add_left(Nat.mul(i, 1n+p), Nat.sub(completion, previous), previous,
    (%N.le_div_iff_mul_le(i, Nat.sub(completion, previous), p)
      : {_ == True{} : Bool}; hi))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=bend-mathlib@0.8.1.0/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_le_add_left
  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=le_div_iff_mul_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=sub_add_cancel