Commit 2023-01-13 09:36 ae3c1ad1

View on Github →

feat: Port/data.nat.succ_pred (#1480)

Estimated changes

added theorem Fin.coe_covby_iff
added theorem Nat.pred_eq_pred
added theorem Nat.pred_iterate
added theorem Nat.succ_eq_succ
added theorem Nat.succ_iterate