proposition: Lemma Db_over_a_casoratian (i j : nat) : (2 <= j)%N -> (j <= i)%N -> b_over_a_seq i - b_over_a_seq j = \sum_(j <= k < i) 6%:Q / (k%:Q + 1) ^ 3 / (a (int.shift 1 k) * a k).
proof: Proof. move=> le2j leji; rewrite -(telescope_nat (fun k => b_over_a_seq (Posz k))) //. rewrite [RHS]big_nat_cond [LHS]big_nat_cond; apply: eq_bigr => k Hk. rewrite -ba_casoratianE /b_over_a_seq /ba_casoratian; last ring_lia. by rewrite PoszD int.zshiftP; field; rewrite !a_neq0. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics shift rat_of_Z seq_defs initial_conds algo_closures reduce_order a_props