Theorem ne_of_irrefl'

feat(order/rel_classes): Unbundled typeclass to state that two relations are the non strict and strict versions (#11381) …