def fixed_rate_future

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

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

47def fixed_rate_future(+previous: Nat, +completion: Nat, +p: Nat,
48  order: Or(N.le(previous, completion), N.le(completion, previous)))
49  -> N.lt(completion,
50    Nat.add(previous, Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p))):
51  match order:
52    case Inl{h}:
53      %N.add_sub_of_le(previous, completion, h)
54        : N.lt(_, Nat.add(previous,
55          Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p)))
56      N.add_lt_add_left(Nat.sub(completion, previous),
57        Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p), previous,
58        quotient_future(Nat.sub(completion, previous), p))
59    case Inr{+h}:
60      %Equal.sym(Nat, Nat.sub(completion, previous), 0n,
61        N.sub_eq_zero_of_le(completion, previous, h))
62        : N.lt(completion, Nat.add(previous, Nat.mul(1n+Nat.div(_, 1n+p), 1n+p)))
63      %Equal.sym(Nat, Nat.add(p, 0n), p, N.add_zero(p))
64        : N.lt(completion, Nat.add(previous, 1n+_))
65      N.lt_of_le_of_lt(completion, previous, Nat.add(previous, 1n+p), h,
66        N.lt_add_of_pos_right(previous, p))