proposition: Theorem convol_mul_inv_r : ∀ k a a', (a.[0] ≠ 0)%K → a' = series_inv a → (convol_mul a a' (S k) = 0)%K.
proof: Proof. intros k a a' Ha Ha'. unfold convol_mul. pose proof (term_inv_nth_formula k Ha Ha') as Hi. apply rng_mul_compat_l with (c := a.[0]%K) in Hi. symmetry in Hi. rewrite rng_mul_assoc in Hi. rewrite rng_mul_opp_r in Hi. rewrite Ha' in Hi. assert (a.[0] * (¹/ a%ser) .[ 0] = 1)%K as H. simpl; rewrite fld_mul_inv_r; [ reflexivity | auto ]. rewrite H in Hi; clear H. rewrite rng_mul_opp_l, rng_mul_1_l in Hi. rewrite <- Ha' in Hi. eapply rng_add_compat_r in Hi. rewrite rng_add_opp_l in Hi. symmetry in Hi. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite Nat.sub_0_r; auto. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation