proposition: Lemma fibZ2P p : ZtoR (nth Z0 (my_pow m2lmul m2lfib p) 0 + nth Z0 (my_pow m2lmul m2lfib p) 1) = (fib (Pos.to_nat p))%:R.
proof: Proof. rewrite [LHS](_ : _ = m2lmx (my_pow m2lmul m2lfib p) 0 0); last first. by rewrite /m3lmx mxE !eqxx andbT. rewrite my_pow_m2lmul my_powP. have : (1 <= Pos.to_nat p)%N. by apply/leP; rewrite -(Pos2Nat.inj_le xH); apply: Pos.le_1_l. rewrite leq_eqVlt=> /orP[/eqP <- | pge2]. by rewrite expr1z mxE eqxx. case: (Pos.to_nat p) pge2 => [ | [ | {}p]] // _. by rewrite m2lfibP /exprz fibmP mxE. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)