proposition: Lemma rho_rec (i : int) : Posz 2 <= i -> rho (i + 1) = h i%:Q (rho i).
proof: Proof. move=> le2i; rewrite hE. have rhoi_neq0 : rho i != 0 by apply/lt0r_neq0/lt_0_rho/le_trans/le2i. have ai_neq0 : a i != 0 by apply/a_neq0/le_trans/le2i. rewrite -[alpha i%:Q](mulfK rhoi_neq0) -mulrBl; apply: canRL (mulfK _) _ => //. have -> : rho (i + 1) * rho i = a (i + 2) / a i. by rewrite /rho mulrA mulfVK -?addrA //; apply/a_neq0; lia. apply: canLR (mulfK _) _; rewrite // mulrDl -mulrA mulNr /rho divfK //. have c2_neq0 : annotated_recs_c.P_cf2 i != 0. by rewrite /annotated_recs_c.P_cf2 lt0r_neq0 ?exprn_gt0 ?addr_gt0; ring_lia. have -> : a (i + 2) = - (annotated_recs_c.P_cf1 i * a (i + 1) + annotated_recs_c.P_cf0 i * a i) / annotated_recs_c.P_cf2 i. apply: canRL (mulfK _) _; rewrite // [LHS]mulrC. apply/eqP; rewrite -subr_eq0 opprK addrA; apply/eqP. have := a_Sn2 le2i; rewrite /annotated_recs_c.P_horner. by rewrite /punk.horner_seqop /= !int.shift2Z -[_ + 1 + 1]addrA. rewrite /annotated_recs_c.P_cf2 /annotated_recs_c.P_cf1 /annotated_recs_c.P_cf0. rewrite /alpha /beta. by field; ring_lia. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) mathcomp(realalg) CoqEAL(hrel param refinements) CoqEAL(pos binnat binint rational) tactics shift binomialz bigopz rat_of_Z rho_computations seq_defs c_props initial_conds algo_closures