proposition: Theorem term_inv_nth_formula : ∀ k a a', (a.[0] ≠ 0)%K → a' = series_inv a → (a'.[S k] = - a'.[0] * Σ (i = 1, S k), a.[i] * a'.[S k - i])%K.
proof: Proof. intros k a a' Ha Ha'. pose proof (term_inv_nth_gen_formula k O Ha Ha') as H. rewrite Nat.sub_0_r in H. rewrite H; [ idtac | intros HH; discriminate HH ]. apply rng_mul_compat_l. apply summation_compat; intros i Hi. apply rng_mul_compat_l. rewrite Ha'. remember minus as g; simpl; subst g. remember (S k - i)%nat as n eqn:Hn. destruct n. reflexivity. apply rng_mul_compat_l. apply summation_compat; intros j Hj. apply rng_mul_compat_l. apply term_inv_iter_enough; fast_omega Hn Hj. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation