RecurrenceProof.quotient_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 36-45 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=36&end_line=45

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

def quotient_future(+elapsed: Nat, +p: Nat)
  -> N.lt(elapsed, Nat.mul(1n+Nat.div(elapsed, 1n+p), 1n+p)):
  %N.not_is_le(Nat.mul(1n+Nat.div(elapsed, 1n+p), 1n+p), elapsed)
    : {_ == True{} : Bool}
  %N.le_div_iff_mul_le(1n+Nat.div(elapsed, 1n+p), elapsed, p)
    : {Bool.not(_) == True{} : Bool}
  %Equal.sym(Bool, Nat.is_le(1n+Nat.div(elapsed, 1n+p), Nat.div(elapsed, 1n+p)),
    False{}, N.not_le_of_lt(Nat.div(elapsed, 1n+p), 1n+Nat.div(elapsed, 1n+p),
      N.lt_succ_self(Nat.div(elapsed, 1n+p)))) : {Bool.not(_) == True{} : Bool}
  {==}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  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=lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt_succ_self
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=not_is_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=not_le_of_lt