Commit 2025-02-06 18:18 bd4e8e35

View on Github →

feat(Order): lemmas for Order.succ and Order.pred in Fin (#21437) The SuccOrder and PredOrder instances are redefined on Fin n, and equational lemmas are provided. The lemma Fin.exists_castSucc_eq_of_ne_last is renamed Fin.eq_castSucc_of_ne_last (for consistency with Fin.eq_succ_of_ne_zero).

Estimated changes

added theorem Fin.orderPred_apply
added theorem Fin.orderPred_eq
added theorem Fin.orderPred_succ
added theorem Fin.orderPred_zero
added theorem Fin.orderSucc_apply
added theorem Fin.orderSucc_castSucc
added theorem Fin.orderSucc_eq
added theorem Fin.orderSucc_last
deleted theorem Fin.pred_apply
deleted theorem Fin.pred_eq
deleted theorem Fin.succ_apply
deleted theorem Fin.succ_eq