Theorem: Summation over k to n of Product of kth with n-kth Fibonacci Numbers

:$\ds \sum_{k \mathop = 0}^n F_k F_{n - k} = \dfrac {\paren {n - 1} F_n + 2n F_{n - 1} } 5$
where $F_n$ denotes the $n$th Fibonacci number.

Proof:
From Generating Function for Fibonacci Numbers, a generating function for the Fibonacci numbers is:
:$\map G z = \dfrac z {1 - z - z^2}$
Then:
{{begin-eqn}}
{{eqn | l = \map G z
      | r = \dfrac z {1 - z - z^2}
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \paren {\dfrac 1 {1 - \phi z} - \dfrac 1 {1 - \hat \phi z} }
      | c = Partial Fraction Expansion
}}
{{end-eqn}}
where:
:$\phi = \dfrac {1 + \sqrt 5} 2$
:$\hat \phi = \dfrac {1 - \sqrt 5} 2$
Hence:
{{begin-eqn}}
{{eqn | l = \paren {\map G z}^2
      | r = \paren {\dfrac 1 {\sqrt 5} \paren {\dfrac 1 {1 - \phi z} - \dfrac 1 {1 - \hat \phi z} } }^2
      | c = 
}}
{{eqn | r = \dfrac 1 5 \paren {\paren {\dfrac 1 {1 - \phi z} }^2 + \paren {\dfrac 1 {1 - \hat \phi z} }^2 - 2 \dfrac 1 {1 - \phi z} \dfrac 1 {1 - \hat \phi z} }
      | c = 
}}
{{eqn | r = \dfrac 1 5 \paren {\dfrac 1 {\paren {1 - \phi z}^2} + \dfrac 1 {\paren {1 - \hat \phi z}^2} - 2 \dfrac {1 - \hat \phi z + 1 - \phi z} {\paren {1 - \phi z} \paren {1 - \hat \phi z} } }
      | c = 
}}
{{eqn | r = \dfrac 1 5 \paren {\dfrac 1 {\paren {1 - \phi z}^2} + \dfrac 1 {\paren {1 - \hat \phi z}^2} - \dfrac 2 {\paren {1 - \phi z} \paren {1 - \paren {1 - \phi} z} } }
      | c = Definition of $\hat \phi$
}}
{{eqn | r = \dfrac 1 5 \paren {\dfrac 1 {\paren {1 - \phi z}^2} + \dfrac 1 {\paren {1 - \hat \phi z}^2} - \dfrac 2 {1 - z - z^2} }
      | c = after algebra
}}
{{eqn | r = \dfrac 1 5 \paren {\sum_{n \mathop = 0}^\infty \paren {n + 1} \paren {\phi z}^n + \sum_{n \mathop = 0}^\infty \paren {n + 1} \paren {\hat \phi z}^n - \dfrac 2 z \map G z}
      | c = Power Series Expansion for $\dfrac 1 {\paren {1 - z}^2}$
}}
{{eqn | r = \dfrac 1 5 \paren {\sum_{n \mathop = 0}^\infty \paren {n + 1} \paren {\phi^n + \hat \phi^n} z^n - \dfrac 2 z \sum_{n \mathop = 0}^\infty F_n z^n}
      | c = Generating Function for Fibonacci Numbers
}}
{{eqn | r = \dfrac 1 5 \paren {\sum_{n \mathop = 0}^\infty \paren {n + 1} \paren {\phi^n + \hat \phi^n} z^n - 2 \sum_{n \mathop = 0}^\infty F_n z^{n - 1} }
      | c = 
}}
{{eqn | r = \dfrac 1 5 \paren {\sum_{n \mathop = 0}^\infty \paren {n + 1} \paren {\phi^n + \hat \phi^n} z^n - 2 \sum_{n \mathop = 1}^\infty F_{n + 1} z^n}
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \dfrac 1 5 \sum_{n \mathop = 0}^\infty \paren {\paren {n + 1} \paren {\phi^n + \hat \phi^n} - 2 F_{n + 1} } z^n 
      | c = 
}}
{{end-eqn}}
Since the coefficient of $z^n$ in $\paren {\map G z}^2$ is $\ds \sum_{k \mathop = 0}^n F_k F_{n - k}$, by comparing coefficients:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n F_k F_{n - k}
      | r = \dfrac 1 5 \paren {\paren {n + 1} \paren {\phi^n + \hat \phi^n} - 2 F_{n + 1} }
      | c = 
}}
{{eqn | r = \dfrac 1 5 \paren {\paren {n + 1} \paren {\dfrac {\phi^{2 n} - \hat \phi^{2 n} } {\sqrt 5} \times \dfrac {\sqrt 5} {\phi^n - \hat \phi^n} } - 2 F_{n + 1} }
      | c = Difference of Two Squares
}}
{{eqn | r = \dfrac 1 5 \paren {\paren {n + 1} \dfrac {F_{2 n} } {F_n} - 2 F_{n + 1} }
      | c = Euler-Binet Formula
}}
{{eqn | r = \dfrac 1 5 \paren {\paren {n + 1} \dfrac {F_{n - 1} F_n + F_n F_{n + 1} } {F_n} - 2 F_{n + 1} }
      | c = Honsberger's Identity
}}
{{eqn | r = \dfrac 1 5 \paren {\paren {n + 1} \paren {F_{n - 1} + F_{n + 1} } - 2 F_{n + 1} }
      | c = 
}}
{{eqn | r = \dfrac 1 5 \paren {\paren {n + 1} \paren {F_n + 2 F_{n - 1} } - 2 \paren {F_n + F_{n - 1} } }
      | c = {{Defof|Fibonacci Numbers}}
}}
{{eqn | r = \dfrac {\paren {n - 1} F_n + 2n F_{n - 1} } 5
      | c = 
}}
{{end-eqn}}
{{qed}}