Commit 2022-09-30 08:02 af90fef9

feat(data/fin): golf, add lemmas (#16711)

• add fin.range_succ, fin.exists_succ_eq_iff, and fin.range_fin_succ;
• golf fin.eq_succ_of_ne_zero and fin.range_cons.