@@ -84,7 +84,7 @@ mutual
8484 negate (Pos Z) = Pos Z
8585 negate (Pos (S n)) = NegS n
8686 negate (NegS n) = Pos (S n)
87−
87+
8888 (-) = subZ
8989 abs = cast . absZ
9090
@@ -155,3 +155,61 @@ plusCommutativeZ (Pos n) (NegS m) = Refl
155155plusCommutativeZ (NegS n) (Pos m) = Refl
156156plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m
157157
158+minusNatZAntiCommutative : (j, k : Nat) -> negate (minusNatZ j k) = minusNatZ k j
159+minusNatZAntiCommutative Z Z = Refl
160+minusNatZAntiCommutative Z (S k) = Refl
161+minusNatZAntiCommutative (S j) Z = Refl
162+minusNatZAntiCommutative (S j) (S k) = minusNatZAntiCommutative j k
163+
164+negateDistributesPlus : (a, b : ZZ) -> negate (a + b) = (negate a) + (negate b)
165+negateDistributesPlus (Pos Z) b = rewrite plusZeroLeftNeutralZ b in
166+ rewrite plusZeroLeftNeutralZ (negate b) in Refl
167+negateDistributesPlus (Pos (S k)) (Pos Z) = rewrite plusZeroRightNeutral k in Refl
168+negateDistributesPlus (Pos (S k)) (Pos (S j)) = rewrite plusCommutative k (S j) in
169+ rewrite plusCommutative j k in Refl
170+negateDistributesPlus (Pos (S k)) (NegS j) = minusNatZAntiCommutative k j
171+negateDistributesPlus (NegS k) (Pos Z) = rewrite plusZeroRightNeutral k in Refl
172+negateDistributesPlus (NegS k) (Pos (S j)) = minusNatZAntiCommutative j k
173+negateDistributesPlus (NegS k) (NegS j) = rewrite plusCommutative k (S j) in
174+ rewrite plusCommutative k j in Refl
175+
176+lemmaMinusSucc : (k, j, i : Nat) -> plusZ (minusNatZ k (S j)) (Pos i) = plusZ (minusNatZ k (S (S j))) (Pos (S i))
177+lemmaMinusSucc Z j i = Refl
178+lemmaMinusSucc (S Z) Z i = Refl
179+lemmaMinusSucc (S (S k)) Z i = rewrite plusCommutative k (S i) in
180+ rewrite plusCommutative i k in Refl
181+lemmaMinusSucc (S k) (S j) i = lemmaMinusSucc k j i
182+
183+lemmaAssocNegation : (k : Nat) -> (c, r : ZZ) -> (Pos (S k)) + (c + r) = ((Pos (S k)) + c) + r -> (NegS k) + ((negate c) + (negate r)) = ((NegS k) + (negate c)) + (negate r)
184+lemmaAssocNegation k c r prf = rewrite sym $ negateDistributesPlus c r in
185+ rewrite sym $ negateDistributesPlus (Pos (S k)) (plusZ c r) in
186+ rewrite sym $ negateDistributesPlus (Pos (S k)) c in
187+ rewrite sym $ negateDistributesPlus (plusZ (Pos (S k)) c) r in
188+ cong $ prf
189+
190+lemmaAssocPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) + (c + r) = ((Pos k) + c) + r
191+lemmaAssocPos k (Pos j) (Pos i) = cong $ plusAssociative k j i
192+lemmaAssocPos k (Pos Z) (NegS i) = rewrite plusZeroRightNeutral k in Refl
193+lemmaAssocPos k (Pos (S j)) (NegS Z) = rewrite plusCommutative k (S j) in
194+ rewrite plusCommutative j k in Refl
195+lemmaAssocPos k (Pos (S j)) (NegS (S i)) = let ind = lemmaAssocPos k (assert_smaller (Pos (S j)) (Pos j)) (assert_smaller (NegS (S i)) (NegS i)) in
196+ rewrite ind in
197+ rewrite plusCommutative k (S j) in
198+ rewrite plusCommutative j k in Refl
199+lemmaAssocPos k (NegS j) (Pos Z) = rewrite plusZeroRightNeutralZ (minusNatZ k (S j)) in Refl
200+lemmaAssocPos Z (NegS Z) (Pos (S i)) = Refl
201+lemmaAssocPos (S k) (NegS Z) (Pos (S i)) = rewrite plusCommutative k (S i) in
202+ rewrite plusCommutative k i in Refl
203+lemmaAssocPos k (NegS (S j)) (Pos (S i)) = let ind = lemmaAssocPos k (assert_smaller (NegS (S j)) (NegS j)) (assert_smaller (Pos (S i)) (Pos i)) in
204+ rewrite ind in
205+ rewrite lemmaMinusSucc k j i in Refl
206+lemmaAssocPos Z (NegS j) (NegS i) = Refl
207+lemmaAssocPos (S k) (NegS Z) (NegS i) = Refl
208+lemmaAssocPos (S k) (NegS (S j)) (NegS i) = let ind = lemmaAssocPos (assert_smaller (S k) k) (assert_smaller (NegS (S j)) (NegS j)) (NegS i) in
209+ rewrite ind in Refl
210+
211+plusAssociativeZ : (l, c, r : ZZ) -> l + (c + r) = (l + c) + r
212+plusAssociativeZ (Pos k) c r = lemmaAssocPos k c r
213+plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in
214+ rewrite sym $ doubleNegElim r in
215+ lemmaAssocNegation k (negate c) (negate r) (lemmaAssocPos (S k) (negate c) (negate r))