refactor: make Order.pred_eq_sub_one a simp lemma (#35742) Sister PR to #35741.
Order.pred_eq_sub_one