module HomeworkFour
%default total
%access public export

even : Nat -> Bool
even Z = True
even (S Z) = False
even (S (S n)) = even n

evenSuc : even n = True -> even (S n) = False
evenSuc {n=Z} Refl = Refl
evenSuc {n=S Z} Refl impossible
evenSuc {n=S (S m)} p = evenSuc {n=m} p

oddSuc : even n = False -> even (S n) = True
oddSuc {n=Z} Refl impossible
oddSuc {n=S Z} Refl = Refl
oddSuc {n=S (S m)} p = oddSuc {n=m} p

evenFlip : even n = b -> even (S n) = not b
evenFlip {n=Z} Refl = Refl
evenFlip {n=S Z} Refl = Refl
evenFlip {n=S (S m)} p = evenFlip {n=m} p

evenFlip' : even n = b -> even (S n) = not b
evenFlip' {b=True} p = evenSuc p
evenFlip' {b=False} p = oddSuc p

evenSucSuc : even n = True -> even (S (S n)) = True
evenSucSuc p = p

oddSucSuc : even n = False -> even (S (S n)) = False
oddSucSuc p = p

evenStay : even n = b -> even (S (S n)) = b
evenStay p = p

evenStayEq : even n = even (S (S n))
evenStayEq = Refl