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
).