Library hydras.Prelude.OrdNotations

Reserved Notation "x 'o<' y" (at level 70, no associativity).
Reserved Notation "x 'o<=' y" (at level 70, no associativity).
Reserved Notation "x 'o>=' y" (at level 70, no associativity).
Reserved Notation "x 'o>' y" (at level 70, no associativity).

Reserved Notation "x 'o<=' y 'o<=' z" (at level 70, y at next level).
Reserved Notation "x 'o<=' y 'o<' z" (at level 70, y at next level).
Reserved Notation "x 'o<' y 'o<' z" (at level 70, y at next level).
Reserved Notation "x 'o<' y 'o<=' z" (at level 70, y at next level).