mathlib3

feat(order/initial_seg): initial and principal segments for `sum.lex` and `prod.lex`

#15368

Open