Commit 2025-07-05 10:59 bfdf54ea

View on Github →

feat(Order/InitialSeg): InitialSeg.exists_sum_relIso (#26772) If r ≼i s, there exists some t with Sum.Lex r t ≃r s. In other words, ordinal subtraction exists.

Estimated changes