proposition: Theorem series_mul_inv_r : ∀ a, (a.[0] ≠ 0)%K → (a * ¹/ a = 1)%ser.
proof: Proof. intros a Ha. constructor; intros i; simpl. destruct i; simpl. unfold convol_mul; simpl. rewrite summation_only_one; simpl. rewrite fld_mul_inv_r; [ reflexivity | assumption ]. apply convol_mul_inv_r; [ assumption | reflexivity ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation