proposition: Lemma is_derive_n_inv_pow : forall m, (0 < m)%nat -> forall n x, x <> 0 -> is_derive_n (fun x => / x ^ m)%R n x (\big[Rmult/1%R]_(i < n) - INR (m + i) / x ^ (m + n))%R.
proof: Proof. move=> m Hm; help_is_derive_n n x. - move=> x Hx; rewrite big1 /= ?addn0; first by field; apply: pow_nonzero. by case. - move=> Hx; auto_derive; first by apply: pow_nonzero. rewrite big_ord_recl big_ord0 /= addn0 addn1 /= Rmult_1_l Rmult_1_r. apply: Rdiv_eq_reg. rewrite -(prednK Hm); simpl; ring. apply: Rmult_neq0; exact: pow_nonzero. by apply: Rmult_neq0; try apply: pow_nonzero. - exact: open_neq. - move=> t Ht; auto_derive; first exact: pow_nonzero. rewrite [in RHS]big_ord_recr /= /Rdiv; rewrite Rmult_assoc; congr Rmult. rewrite Rmult_1_l; apply: Rdiv_eq_reg; first last. exact: pow_nonzero. apply: Rmult_neq0; exact: pow_nonzero. rewrite !addnS /=; ring. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp