diff --git a/theories/ordered_qelim.v b/theories/ordered_qelim.v
index 11b9f8a..a2c776f 100644
--- a/theories/ordered_qelim.v
+++ b/theories/ordered_qelim.v
@@ -172,15 +172,14 @@ Declare Scope oclause_scope.
 Delimit Scope oclause_scope with OCLAUSE.
 Open Scope oclause_scope.
 
-Notation "p .1" := (@eq_of_oclause _ p)
-  (at level 2, left associativity, format "p .1") : oclause_scope.
-Notation "p .2" := (@neq_of_oclause _ p)
-  (at level 2, left associativity, format "p .2") : oclause_scope.
+(* TODO: add `at level 1, left associativity` when dropping the support for Coq 8.19 *)
+Notation "p .1" := (@eq_of_oclause _ p) (format "p .1") : oclause_scope.
+Notation "p .2" := (@neq_of_oclause _ p) (format "p .2") : oclause_scope.
 
 Notation "p .3" := (@lt_of_oclause _ p)
-  (at level 2, left associativity, format "p .3") : oclause_scope.
+  (at level 1, left associativity, format "p .3") : oclause_scope.
 Notation "p .4" := (@le_of_oclause _ p)
-  (at level 2, left associativity, format "p .4") : oclause_scope.
+  (at level 1, left associativity, format "p .4") : oclause_scope.
 
 Definition oclause_eq (T : eqType)(t1 t2 : oclause T) :=
   let: Oclause eq_l1 neq_l1 lt_l1 leq_l1 := t1 in