@@ -89,3 +89,75 @@ mutual
8989 oddOdd : Odd n -> odd n = True
9090 oddOdd {n = Z} (_ ** pf) = absurd pf
9191 oddOdd {n = S _} pf = evenEven $ predOddEven pf
92+
93+||| Even plus Even is Even.
94+evenPlusEven : Even j -> Even k -> Even (j + k)
95+evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =
96+ rewrite pf_j in
97+ rewrite pf_k in
98+ (half_j + half_k **
99+ sym $ multDistributesOverPlusLeft half_j half_k 2)
100+
101+||| Odd plus Odd is Even.
102+oddPlusOdd : Odd j -> Odd k -> Even (j + k)
103+oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =
104+ rewrite pf_j in
105+ rewrite pf_k in
106+ rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in
107+ rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in
108+ (S (haf_j + haf_k) ** Refl)
109+
110+||| Even plus Odd is Odd.
111+evenPlusOdd : Even j -> Odd k -> Odd (j + k)
112+evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =
113+ rewrite pf_j in
114+ rewrite pf_k in
115+ rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in
116+ rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in
117+ (half_j + haf_k ** Refl)
118+
119+||| A helper fact.
120+multShuffle : (a, b, c : Nat) ->
121+ (a * c) * (b * c) = ((a * b) * c) * c
122+multShuffle a b c =
123+ rewrite multAssociative (a * c) b c in
124+ rewrite multCommutative (a * c) b in
125+ rewrite multAssociative b a c in
126+ rewrite multCommutative b a in
127+ Refl
128+
129+||| Even times Even is Even.
130+evenMultEven : Even j -> Even k -> Even (j * k)
131+evenMultEven (half_j ** pf_j) (half_k ** pf_k) =
132+ rewrite pf_j in
133+ rewrite pf_k in
134+ (half_j * half_k * 2 **
135+ multShuffle half_j half_k 2)
136+
137+||| Even times Odd is Even.
138+evenMultOdd : Even j -> Odd k -> Even (j * k)
139+evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =
140+ let half = half_j * haf_k * 2 in
141+ rewrite pf_j in
142+ rewrite pf_k in
143+ rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in
144+ rewrite multShuffle half_j haf_k 2 in
145+ (half_j + half **
146+ sym $ multDistributesOverPlusLeft half_j half 2)
147+
148+||| Odd times Odd is Odd.
149+oddMultOdd : Odd j -> Odd k -> Odd (j * k)
150+oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =
151+ let
152+ haf = haf_j * haf_k * 2
153+ rem = haf_j + haf_k
154+ in
155+ rewrite pf_j in
156+ rewrite pf_k in
157+ rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in
158+ rewrite multShuffle haf_j haf_k 2 in
159+ rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in
160+ rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in
161+ rewrite plusCommutative haf_k haf_j in
162+ rewrite sym $ multDistributesOverPlusLeft rem haf 2 in
163+ (rem + haf ** Refl)