proposition: Corollary sum_aV_bis (n : nat) : \sum_(0 <= i < n.+1) ((a i).-1)%:Q / (a_rat i) = n.+1%:Q - (a_rat n.+1 - 2%:Q) / (a_rat n.+1 - 1).
proof: Proof. have -> : \sum_(0 <= i < n.+1) ((a i).-1)%:Q / a_rat i = \sum_(0 <= i < n.+1) (1 - (a_rat i) ^-1). apply: eq_bigr => i _; rewrite /a_rat. by case: (a i) (a_pos i) => //= ai _; field; ring_lia. by rewrite sumrB big_mkord sumr_const /= card_ord sum_aV. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial