Proof of `Integral start times suffice`
groundedproofs/Lax391470Proofs/IntegralStartTimes.lean · lax-391470
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Round every start time up. Rounding up is monotone and commutes with adding an integer, and all data are integers, so every inequality of feasibility survives.