A sea of simple induction.

During week 1, we dived straight into a sea of induction, the fundamental concept of computational logic in the class. As a smooth transition from the three month summer vocation to the busy study season, our good friend: simple induction was introduced to us first. Examples of simple induction presented in the class were familiar yet interesting. The rightmost digit of 3^n reinforced the idea of appropriate base cases and the number of odd subsets of a set introduced, for the first time, a brand-new way of inductive thinking. After digging some dusted memories of CSC165, I did not have a hard time comprehending those examples.
Here is a simple exercise I did to understand the mechanism of simple induction. I used the structural proof I learned in CSC165.

Claim: There are no more than two consecutive elements of the Fibonacci sequence that have remainder 1 when divided by 7.

Proof using simple induction:
\forall i \in N, (mod(F(i), 7) = 1 \and mod(F(i+1), 7) = 1) \implies mod(F(i+2), 7) != 1.
Assume i \in N
Assume mod(F(i), 7) = 1 \and mod(F(i+1), 7) = 1
Then mod(F(i+2), 7) = mod(F(i) + F(i+1), 7)
# The property of the element in the Fibonacci sequence.
Then mod(F(i) + F(i+1), 7) = mod(mod(F(i), 7) + mod(F(i+1), 7), 7)
Then mod(mod(F(i), 7) + mod(F(i+1), 7), 7) = mod(1+1, 7) = 2
Then mod(F(i+2), 7) = 2
Then mod(F(i+2), 7) != 1
Then (mod(F(i), 7) = 1 \and mod(F(i+1), 7) = 1) \implies mod(F(i+2), 7) != 1
Then \forall i \in N, (mod(F(i), 7) = 1 \and mod(F(i+1), 7) = 1) \implies mod(F(i+2), 7) != 1