proposition: Theorem fibr_prop8 (fr := fun n => (BR_phi ^r n -r ((BRopp (BRinv BR_phi)))^r n)/r (BRsqrt \5r)): forall n, natp n -> fr n = BR_of_Q (BQ_of_Z (BZ_of_nat (Fib n))) .
proof: Proof. pose ff := fun n => BR_of_Q (BQ_of_Z (BZ_of_nat (Fib n))). suff: forall n, natp n -> fr n = ff n /\ fr (csucc n) = ff (csucc n). by move => H n nN; case: (H n nN). have pa:= RS_phi. have pb:realp (BRopp (BRinv BR_phi)) by apply:RSo; apply: RS_inv. move:(BRsqrt_prop (BRps_sBRp RpsS5)) => [pc /BRp_sBR pd]. have pe:BRsqrt \5r <> \0r. by move => h; move:(BRps_nz RpsS5); rewrite pc h /BRsquare BRprod_0l. apply: Nat_induction. rewrite /fr/ff succ_zero Fib0 Fib1 -/BR_zero -/BR_one BRnpowx0 (BRnpowx1 pa). rewrite BRnpowx0 (BRnpowx1 pb) (BRdiff_xx RS1) /BRdiff {1}/BRdiv. rewrite (BRopp_K (RS_inv pa)) fibr_prop5 BRdiv_xx // BRprod_0l //. move => n nN [ha hb]; split => //. have hc := (NS_succ nN);have hc' := (NS_succ hc). have ->: ff (csucc (csucc n)) = fr n +r fr (csucc n). move:(NS_Fib nN) (NS_Fib hc) (NS_Fib hc') => qa qb qc. move:(BZ_of_nat_i qa)(BZ_of_nat_i qb) (BZ_of_nat_i qc) => ra rb rc. move:(BQ_of_Z_iQ ra)(BQ_of_Z_iQ rb) (BQ_of_Z_iQ rc) => sa sb sc. by rewrite ha hb /ff (Fib_rec nN) - BZsum_cN // - BQsum_cZ// BRsum_cQ //. move: fibr_prop3 fibr_prop6 => qa qb. have qc: realp (BR_phi ^r n -r BRopp (BRinv BR_phi) ^r n). by apply: RS_diff;apply:RS_Brnpow. have qd:realp (BR_phi ^r csucc n -r BRopp (BRinv BR_phi) ^r csucc n). by apply: RS_diff;apply:RS_Brnpow. have qc':= (RS_Brnpow RS_phi hc). have qd1':= (RS_Brnpow pb hc); have qd':= RSo qd1'. have qd1'':= (RS_Brnpow pb nN); have qd'':= RSo qd1''. have qc'':= (RS_Brnpow RS_phi nN). rewrite/fr BRsumC - BRdiv_sumDl // /BRdiff BRsum_ACA // - BRoppD //. by rewrite - (fibr_prop7 RS_phi qa nN) -(fibr_prop7 pb qb nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)