mathlib

0ec9cd8d - chore(data/fin): add simp lemmas about 1 and cast_{pred, succ} (#7067)