Commit 2023-01-13 10:17 6d0f7fe0

View on Github →

Feat: Port/data.fin.succ_pred (#1511) Port of data.fin.succ_pred to Data.Fin.SuccPred

Estimated changes

added theorem Fin.pred_apply
added theorem Fin.pred_eq
added theorem Fin.succ_apply
added theorem Fin.succ_eq