theorem bounded_update_stays_between_state_and_target
theorem bounded_update_stays_between_state_and_target
: ∀ (state target eta : Int),
  state ≤ target → state ≤ boundedAdaptationUpdate state target eta ∧ boundedAdaptationUpdate state target eta ≤ target