Documentation

Mathlib.Data.Sum.Order