|
0
|
1 open import Relation.Binary.PropositionalEquality
|
|
|
2 open import nat
|
|
|
3 open import nat_add
|
|
5
|
4 open !$\equiv$!-Reasoning
|
|
0
|
5
|
|
|
6 module nat_add_sym_reasoning where
|
|
|
7
|
|
5
|
8 addToRight : (n m : Nat) !$\rightarrow$! S (n + m) !$\equiv$! n + (S m)
|
|
0
|
9 addToRight O m = refl
|
|
|
10 addToRight (S n) m = cong S (addToRight n m)
|
|
|
11
|
|
5
|
12 addSym : (n m : Nat) !$\rightarrow$! n + m !$\equiv$! m + n
|
|
0
|
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
|
|
5
|
17 (S n) + (S m) !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
|
18 S (n + S m) !$\equiv$!!$\langle$! cong S (addSym n (S m)) !$\rangle$!
|
|
|
19 S ((S m) + n) !$\equiv$!!$\langle$! addToRight (S m) n !$\rangle$!
|
|
|
20 S (m + S n) !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
|
21 (S m) + (S n) !$\blacksquare$!
|
