Commit 2022-02-02 14:51 cd1d839a

feat(order/rel_classes): Unbundled typeclass to state that two relations are the non strict and strict versions (#11381) This defines a Prop-valued mixin is_nonstrict_strict_order α r s to state s a b ↔ r a b ∧ ¬ r b a. The idea is to allow dot notation for lemmas about the interaction of ⊆ and ⊂ (which currently do not have a preorder-like typeclass). Dot notation on each of them is already possible thanks to unbundled relation classes (which allow to state lemmas for both set and finset).