proposition: Lemma ba_casoratianE (n : int) : 2%:~R <= n -> ba_casoratian n = 6%:Q / (n%:Q + 1) ^ 3.
proof: Proof. move=> le2n; have le0n : 0 <= n by exact: le_trans le2n. pose v (k : int) : rat := 6%:Q / (k%:Q + 1) ^ 3. pose c1 := annotated_recs_c.P_cf2. pose c0 := annotated_recs_c.P_cf0. pose Urec (v : int -> rat) := forall (k : int), 2%:~R <= k -> c1 k * v (int.shift 1 k) - c0 k * v k = 0. have uUrec : Urec ba_casoratian. move=> k le2k; have le0k : 0 <= k by exact: le_trans le2k. have brec := b_Sn2 le0k; have arec := a_Sn2 le2k. have -> : 0 = a (int.shift 1 k) * annotated_recs_c.P_horner b k - b (int.shift 1 k) * annotated_recs_c.P_horner a k. by rewrite brec arec !mulr0 subrr. rewrite /annotated_recs_c.P_horner /annotated_recs_c.P_seq /c1 /c0. by rewrite /punk.horner_seqop /= /ba_casoratian; ring. have vUrec : Urec v. move=> k le2k. rewrite /c0 /c1 /annotated_recs_c.P_cf2 /annotated_recs_c.P_cf0 /v. by rewrite int.shift2R; field; ring_lia. suff {uUrec vUrec v} Urec1P (w1 w2 : int -> rat) : w1 2 = w2 2 -> Urec w1 -> Urec w2 -> forall (k : int), 2%:~R <= k -> w1 k = w2 k. apply: (Urec1P _ v) => //; rewrite /ba_casoratian /v b2_eq b3_eq. rewrite int.shift2Z a2_eq a3_eq. by field; ring_lia. have hUrec w k : Urec w -> 2%:~R <= k -> w (int.shift 1 k) = (c0 k / c1 k) * w k. move=> wUrec le2k; rewrite mulrAC; apply: canRL (mulfK _) _. by rewrite /c1 /annotated_recs_c.P_cf2 expf_eq0; ring_lia. by apply/eqP; rewrite [_ * c1 k]mulrC -subr_eq0 wUrec. move=> ic Uw1 Uw2 [] //; elim => // [[]] // [] // k ihk _. by rewrite -[_.+3]addn1 PoszD -int.zshiftP !hUrec // ihk. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics shift rat_of_Z seq_defs initial_conds algo_closures reduce_order a_props