refactor(order/rel_classes): ditch `is_extensional` (#15373)
This typeclass was barely used anyways, and the instances that existed for it had unnecessary assumptions. We replace it by the theorem `extensional_of_trichotomous_of_irrefl`.
A relevant short discussion on this typeclass: [link](https://github.com/leanprover-community/mathlib/pull/15371#issuecomment-1185138800)
