@@ -39,43 +39,32 @@ private
39
39
40
40
open import Data.Nat.Divisibility.Core public hiding (*-pres-∣)
41
41
42
- module _ (m∣n : m ∣ n) where
43
-
44
- open _∣_ m∣n
45
-
46
- quotient≢0 : .{{NonZero n}} → NonZero quotient
47
- quotient≢0 rewrite equality = m*n≢0⇒m≢0 quotient
48
-
49
- equalityᵒ : n ≡ m * quotient
50
- equalityᵒ rewrite equality = *-comm quotient m
51
-
52
- quotient-∣ : quotient ∣ n
53
- quotient-∣ = divides m equalityᵒ
54
-
55
- quotient>1 : m < n → 1 < quotient
56
- quotient>1 m<n = *-cancelˡ-< m 1 quotient $ begin-strict
57
- m * 1 ≡⟨ *-identityʳ m ⟩
58
- m <⟨ m<n ⟩
59
- n ≡⟨ equalityᵒ ⟩
60
- m * quotient ∎
61
- where open ≤-Reasoning
62
-
63
- quotient-< : .{{NonTrivial m}} → .{{NonZero n}} → quotient < n
64
- quotient-< = begin-strict
65
- quotient <⟨ m<m*n quotient m (nonTrivial⇒n>1 m) ⟩
66
- quotient * m ≡⟨ equality ⟨
67
- n ∎
68
- where
69
- open ≤-Reasoning
70
- instance _ = quotient≢0
71
-
72
- -- Exports
73
-
74
- open _∣_ using (quotient) public
75
-
42
+ quotient≢0 : (m∣n : m ∣ n) → .{{NonZero n}} → NonZero (quotient m∣n)
43
+ quotient≢0 m∣n rewrite _∣_.equality m∣n = m*n≢0⇒m≢0 (quotient m∣n)
44
+
45
+ equalityᵒ : (m∣n : m ∣ n) → n ≡ m * (quotient m∣n)
46
+ equalityᵒ {m = m} m∣n rewrite _∣_.equality m∣n = *-comm (quotient m∣n) m
47
+
48
+ quotient-∣ : (m∣n : m ∣ n) → (quotient m∣n) ∣ n
49
+ quotient-∣ {m = m} m∣n = divides m (equalityᵒ m∣n)
50
+
51
+ quotient>1 : (m∣n : m ∣ n) → m < n → 1 < quotient m∣n
52
+ quotient>1 {m} {n} m∣n m<n = *-cancelˡ-< m 1 (quotient m∣n) $ begin-strict
53
+ m * 1 ≡⟨ *-identityʳ m ⟩
54
+ m <⟨ m<n ⟩
55
+ n ≡⟨ equalityᵒ m∣n ⟩
56
+ m * quotient m∣n ∎
57
+ where open ≤-Reasoning
58
+
59
+ quotient-< : (m∣n : m ∣ n) → .{{NonTrivial m}} → .{{NonZero n}} → quotient m∣n < n
60
+ quotient-< {m} {n} m∣n = begin-strict
61
+ quotient m∣n <⟨ m<m*n (quotient m∣n) m (nonTrivial⇒n>1 m) ⟩
62
+ quotient m∣n * m ≡⟨ _∣_.equality m∣n ⟨
63
+ n ∎
64
+ where open ≤-Reasoning ; instance _ = quotient≢0 m∣n
76
65
77
66
------------------------------------------------------------------------
78
- -- Relating _/_ and _∣_. quotient
67
+ -- Relating _/_ and quotient
79
68
80
69
n/m≡quotient : (m∣n : m ∣ n) .{{_ : NonZero m}} → n / m ≡ quotient m∣n
81
70
n/m≡quotient {m = m} (divides-refl q) = m*n/n≡m q m
0 commit comments