mathlib3

65ee8572 - feat(order/extension/well): Extend a well-founded order (#17054)

feat(order/extension/well): Extend a well-founded order (#17054) A well-founded order can be extended to a well order. For this, we need the rank of an an element of a well-founded order. Also rename `order.extension` to `order.extension.linear`. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>