pub open spec fn integer_in_range<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64>( value: int, ) -> bool
{ &&& (HAS_MIN ==> MIN as int <= value) &&& (HAS_MAX ==> value <= MAX as int) }