def quotient_future

bend-kit-scheduler@0.4.1.0 · recurrence_proof.bend:36

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

36def quotient_future(+elapsed: Nat, +p: Nat)
37  -> N.lt(elapsed, Nat.mul(1n+Nat.div(elapsed, 1n+p), 1n+p)):
38  %N.not_is_le(Nat.mul(1n+Nat.div(elapsed, 1n+p), 1n+p), elapsed)
39    : {_ == True{} : Bool}
40  %N.le_div_iff_mul_le(1n+Nat.div(elapsed, 1n+p), elapsed, p)
41    : {Bool.not(_) == True{} : Bool}
42  %Equal.sym(Bool, Nat.is_le(1n+Nat.div(elapsed, 1n+p), Nat.div(elapsed, 1n+p)),
43    False{}, N.not_le_of_lt(Nat.div(elapsed, 1n+p), 1n+Nat.div(elapsed, 1n+p),
44      N.lt_succ_self(Nat.div(elapsed, 1n+p)))) : {Bool.not(_) == True{} : Bool}
45  {==}