mathlib3

08931580 - refactor(order/rel_classes): redefine `is_well_order` in terms of `is_well_founded` (#15729)

refactor(order/rel_classes): redefine `is_well_order` in terms of `is_well_founded` (#15729) We redefine `is_well_order` in terms of `is_well_founded`, and remove the redundant `is_irrefl` assumption in the process. This also replaces `is_well_order.wf` with `is_well_founded.wf`.