proposition: Theorem term_inv_nth_gen_formula : ∀ k a a' i, (a.[0] ≠ 0)%K → a' = series_inv a → (S k - i ≠ 0)%nat → (a'.[S k - i] = - a'.[0] * Σ (j = 1, S k - i), a.[j] * term_inv (S k) a (S k - i - j))%K.
proof: Proof. intros k a a' i Ha Ha' Hki. rewrite Ha'. remember minus as g; simpl; subst g. destruct (zerop (S k - i)) as [| H₁]; [ contradiction | idtac ]. remember (S k - i)%nat as ki eqn:Hki₂. destruct ki. exfalso; apply Hki; reflexivity. clear H₁. apply rng_mul_compat_l. rewrite summation_succ_succ. apply summation_compat; intros j Hj. apply rng_mul_compat_l. remember minus as g; simpl; subst g. rewrite Nat.sub_succ. remember (ki - j)%nat as n eqn:Hn. destruct n. reflexivity. apply rng_mul_compat_l. apply summation_compat; intros l Hl. apply rng_mul_compat_l. apply term_inv_iter_enough; [ fast_omega Hl Hn | idtac ]. rewrite <- Nat.sub_succ, Hki₂ in Hn. rewrite <- Nat.sub_succ, Hn. rewrite <- Nat.sub_add_distr. rewrite Nat.add_succ_l. rewrite Nat_sub_sub_comm, Nat.sub_succ. rewrite <- Nat.sub_add_distr. apply Nat.le_sub_l. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation