|
7
|
1 open import Relation.Binary.PropositionalEquality
|
|
|
2 open import nat
|
|
|
3 open import nat_add
|
|
|
4 open ≡-Reasoning
|
|
|
5
|
|
|
6 module nat_add_sym_reasoning where
|
|
|
7
|
|
|
8 addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m)
|
|
|
9 addToRight O m = refl
|
|
|
10 addToRight (S n) m = cong S (addToRight n m)
|
|
|
11
|
|
|
12 addSym : (n m : Nat) -> n + m ≡ m + n
|
|
|
13 addSym O O = refl
|
|
|
14 addSym O (S m) = cong S (addSym O m)
|
|
|
15 addSym (S n) O = cong S (addSym n O)
|
|
|
16 addSym (S n) (S m) = begin
|
|
|
17 (S n) + (S m) ≡⟨ refl ⟩
|
|
|
18 S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩
|
|
|
19 S ((S m) + n) ≡⟨ addToRight (S m) n ⟩
|
|
|
20 S (m + S n) ≡⟨ refl ⟩
|
|
|
21 (S m) + (S n) ∎
|
