renaming slt_irrN into sltnn

imdea-software · Aug 29, 2024 · af748a8 · af748a8
1 parent b426ffe
commit af748a8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/core/useqord.v b/core/useqord.v
@@ -103,7 +103,7 @@ Lemma slt_irr x ks : x <[ks] x = false.
 Proof. by rewrite seqlt_unlock; apply: ltnn. Qed.
 
 (* non-equational variant *)
-Lemma slt_irrN x ks : ~ x <[ks] x.
+Lemma sltnn x ks : ~ x <[ks] x.
 Proof. by rewrite slt_irr. Qed.
 
 (****************** antisymmetry ****************)