proposition: Lemma sum_aV (n : nat) : \sum_(0 <= i < n.+1) (a i)%:Q ^-1 = ((a n.+1)%:Q - 2%:Q) / ((a n.+1)%:Q - 1).
proof: Proof. elim: n => [|n ihn]; first by rewrite big_mkord big_ord1. pose an1 := (a n.+1)%:Q; pose an2 := (a n.+2)%:Q. suff step : (an1 - 2%:Q) / (an1 - 1) + an1 ^-1 = (an2 - 2%:Q) / (an2 - 1). by rewrite big_nat_recr // ihn /= step. rewrite [an2]a_rat_rec1 /an1 addrK. by field; rewrite pmulrn !lt0r_neq0. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial