We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 618a6a9 commit a4fbbc6Copy full SHA for a4fbbc6
1 file changed
src/Data/Nat/Divisibility.agda
@@ -349,12 +349,12 @@ hasNonTrivialDivisor-≢ d≢n d∣n
349
350
hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n → m ∣ o →
351
o HasNonTrivialDivisorLessThan n
352
-hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) n∣o
353
- = hasNonTrivialDivisor d<n (∣-trans d∣m n∣o)
+hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) m∣o
+ = hasNonTrivialDivisor d<n (∣-trans d∣m m∣o)
354
355
-- Monotonicity wrt ≤
356
357
hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o →
358
m HasNonTrivialDivisorLessThan o
359
-hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) m≤o
360
- = hasNonTrivialDivisor (<-≤-trans d<n m≤o) d∣m
+hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) n≤o
+ = hasNonTrivialDivisor (<-≤-trans d<n n≤o) d∣m
0 commit comments