File tree Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -872,7 +872,7 @@ module _ {R : Rel A p} (R? : B.Decidable R) where
872
872
length-derun : ∀ xs → length (derun R? xs) ≤ length xs
873
873
length-derun [] = ≤-refl
874
874
length-derun (x ∷ []) = ≤-refl
875
- length-derun (x ∷ y ∷ xs) with ih ← length-derun (y ∷ xs) | does (R? x y)
875
+ length-derun (x ∷ y ∷ xs) with ih ← length-derun (y ∷ xs) | does (R? x y)
876
876
... | true = m≤n⇒m≤1+n ih
877
877
... | false = s≤s ih
878
878
Original file line number Diff line number Diff line change @@ -12,7 +12,7 @@ open import Data.Nat.Base
12
12
open import Data.Nat.DivMod
13
13
open import Data.Nat.Divisibility
14
14
open import Data.Nat.Properties
15
- open import Relation.Binary.Definitions
15
+ open import Relation.Binary.Definitions
16
16
open import Relation.Binary.PropositionalEquality
17
17
using (_≡_; refl; sym; cong; subst)
18
18
@@ -118,7 +118,7 @@ module _ {n k} (k<n : k < n) where
118
118
119
119
[n-k]! = [n-k] !
120
120
[n-k-1]! = [n-k-1] !
121
-
121
+
122
122
[n-k]≡1+[n-k-1] : [n-k] ≡ suc [n-k-1]
123
123
[n-k]≡1+[n-k-1] = +-∸-assoc 1 k<n
124
124
You can’t perform that action at this time.
0 commit comments