From d60c67b8f33f55e11ca159246d2a447102f10f20 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 30 Aug 2019 11:30:21 +0200
Subject: Change the order of arguments in `ltngtP`

from
`ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)`
to
`ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`,
to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.
---
 mathcomp/ssreflect/prime.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/prime.v')

diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 9eafea9..1185e67 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -579,7 +579,7 @@ Qed.
 Lemma coprime_has_primes m n :
   0 < m -> 0 < n -> coprime m n = ~~ has (mem (primes m)) (primes n).
 Proof.
-move=> m_gt0 n_gt0; apply/eqnP/hasPn=> [mn1 p | no_p_mn].
+move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn].
   rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n].
   have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m.
   by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m.
-- 
cgit v1.2.3