[Merged by Bors] - chore(set_theory/ordinal_arithmetic): Make auxiliary result private

[vihdzp]

---

[jcommelin]

Mathlib generally follows the philosophy of making very few things private. Because it happens that such aux lemmas are often useful in ways that the author didn't expect. And making them private makes them harder to discover.

[vihdzp]

Mathlib generally follows the philosophy of making very few things private. Because it happens that such aux lemmas are often useful in ways that the author didn't expect. And making them private makes them harder to discover.

This auxiliary result is made entirely redundant by CNF_pairwise and CNF_fst_le_log. As far as I can see, the only reason it exists is to factor out commonalities in the proofs.

[jcommelin]

Ok, fair enough.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests