proposition: Lemma matrix_fib : forall n, 'M{[:: [::(fib n.+2)%:R; (fib n.+1)%:R]; [::(fib n.+1)%:R; (fib n)%:R]]} = ('M{[:: [:: 1; 1]; [:: 1; 0]]})^+n.+1 :> 'M[R]_(2,2).
proof: Proof. elim=> [|n IH]. by apply/matrixP=> [[[|[|]] // _] [[|[|]] // _]]; rewrite !mxE. rewrite exprS -IH; apply/matrixP=> i j. by rewrite !mxE !big_ord_recl big_ord0 !mxE; case: i=> [[|[|]]] //= _; case: j=> [[|[|]]] //= _; rewrite !mul1r ?mul0r !addr0 // fibSS natrD. Qed.
imports: mathcomp(all_ssreflect all_algebra)