Commit 2024-05-17 17:53 f933e98b
View on Github →feat(Order/RelSeries): add snoc construction (#12915)
Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ and an a such that aₙ -r→ a holds, there is
a series of length n+1: a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a.
These and some other lemmas in this PR are all extracted from Order/JordanHolder.lean