[Merged by Bors] - feat(Data/Fintype/Order): Slightly strengthen Fin.completeLinearOrder.#14616
Closed
linesthatinterlace wants to merge 1 commit intomasterfrom linesthatinterlace/fin_completelinearorder
