proposition: Lemma fibmP n : fibm ^+ n.+2 = \matrix_(i, j) if (val i == 0%N) && (val j == 0%N) then (fib n.+2)%:R else if ((val i + val j == 1)%N) then (fib n.+1)%:R else (fib n)%:R.
proof: Proof. elim: n => [ | n Ih]. rewrite /=. by apply/matrixP=> [][[ | [ | i]] b_i][[ | [ | j]] b_j] //=; rewrite mxE /= expr2 mxE /fibm 2!big_ord_recr /= big_ord0; rewrite !mxE /= ?(add0r, addr0, mulr1, mul1r, mul0r). rewrite exprS Ih. have [fn1 fn1P] : exists fn1, fn1 = fib n.+1 by exists (fib n.+1). have [fn2 fn2P] : exists fn2, fn2 = fib n.+2 by exists (fib n.+2). have [fn3 fn3P] : exists fn3, fn3 = fib n.+3 by exists (fib n.+3). rewrite -!(fn1P, fn2P, fn3P). apply/matrixP=> [][[ | [ | i]] b_i][[ | [ | j]] b_j] //=; rewrite !mxE /= 2!big_ord_recr /= big_ord0 add0r /= !mxE /= ?(add0r, addr0, mulr1, mul1r, mul0r) -?natrD //. by rewrite fn2P fn1P fn3P addnC. by rewrite fn2P fn1P addnC. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)