Indeed rewrite rules do not allow to infer a <= b - 1 from a < b.
Everything that has to do with arithmetic is managed by external prover ML.
So, if you have ML installed and it's selected in auto-tactics, a <= b - 1 will be proved from a < b.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
This Tracker item was closed automatically by the system. It was
previously set to a Pending status, and the original submitter
did not respond within 14 days (the time period specified by
the administrator of this Tracker).
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Indeed rewrite rules do not allow to infer a <= b - 1 from a < b.
Everything that has to do with arithmetic is managed by external prover ML.
So, if you have ML installed and it's selected in auto-tactics, a <= b - 1 will be proved from a < b.
This Tracker item was closed automatically by the system. It was
previously set to a Pending status, and the original submitter
did not respond within 14 days (the time period specified by
the administrator of this Tracker).