mathlib

b799b43d - feat(data/fin/basic): eq_succ_of_ne_zero, coe_cast_pred, succ_pred_above_succ (#16294)

feat(data/fin/basic): eq_succ_of_ne_zero, coe_cast_pred, succ_pred_above_succ (#16294) This PR introduces three basic lemmas about `fin`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>