Commit 2025-12-17 19:48 d24b8b34
View on Github →chore: remove March and April 2025 deprecated declarations (#32990)
I undeprecate Nat.Ico_succ_right_eq_insert_Ico, since it is a natural counterpart to the nondeprecated Nat.Ico_succ_left_eq_erase_Ico.