We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 71bd3f2 commit d8949ceCopy full SHA for d8949ce
src/Data/Nat/Properties.agda
@@ -1633,7 +1633,7 @@ m<n+o⇒m∸n<o (suc m) (suc n) lt = m<n+o⇒m∸n<o m n (s<s⁻¹
1633
m+n≤o⇒m≤o∸n : ∀ m {n o} → m + n ≤ o → m ≤ o ∸ n
1634
m+n≤o⇒m≤o∸n zero le = z≤n
1635
m+n≤o⇒m≤o∸n (suc m) (s≤s le)
1636
- rewrite ∸-suc(m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m le)
+ rewrite ∸-suc (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m le)
1637
1638
m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o
1639
m≤o∸n⇒m+n≤o m z≤n le rewrite +-identityʳ m = le
0 commit comments