begin induction
This commit is contained in:
parent
00ec52d94a
commit
583e0fb344
1 changed files with 14 additions and 1 deletions
|
@ -868,7 +868,17 @@ just apply the previous results which show addition
|
||||||
is associative and commutative.
|
is associative and commutative.
|
||||||
|
|
||||||
```
|
```
|
||||||
-- Your code goes here
|
+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
|
||||||
|
+-swap m n p =
|
||||||
|
begin
|
||||||
|
m + (n + p)
|
||||||
|
≡⟨ sym (+-assoc m n p) ⟩
|
||||||
|
(m + n) + p
|
||||||
|
≡⟨ cong (_+ p) (+-comm m n) ⟩
|
||||||
|
(n + m) + p
|
||||||
|
≡⟨ +-assoc n m p ⟩
|
||||||
|
n + (m + p)
|
||||||
|
∎
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
||||||
|
@ -882,6 +892,9 @@ for all naturals `m`, `n`, and `p`.
|
||||||
|
|
||||||
```
|
```
|
||||||
-- Your code goes here
|
-- Your code goes here
|
||||||
|
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
|
||||||
|
*-distrib-+ zero n p = {! begin (zero + n) * p ≡ zero * p + n * p ∎ !}
|
||||||
|
*-distrib-+ (suc m) n p = {! !}
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue