def due_tick

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

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

75def due_tick(+previous: Nat, +completion: Nat, +p: Nat, +i: Nat,
76  h: N.le(previous, completion), hi: N.le(i, Nat.div(Nat.sub(completion, previous), 1n+p)))
77  -> N.le(Nat.add(previous, Nat.mul(i, 1n+p)), completion):
78  %N.sub_add_cancel(completion, previous, h)
79    : N.le(Nat.add(previous, Nat.mul(i, 1n+p)), _)
80  %N.add_comm(previous, Nat.sub(completion, previous))
81    : N.le(Nat.add(previous, Nat.mul(i, 1n+p)), _)
82  N.add_le_add_left(Nat.mul(i, 1n+p), Nat.sub(completion, previous), previous,
83    (%N.le_div_iff_mul_le(i, Nat.sub(completion, previous), p)
84      : {_ == True{} : Bool}; hi))