proposition: Lemma powerRZ_ind (P : Z -> (R -> R) -> Prop) : P 0%Z (fun x => 1) -> (forall n, P (Z.of_nat n) (fun x => x ^ n)) -> (forall n, P ((-(Z.of_nat n))%Z) (fun x => / x ^ n)) -> (forall f g, f =1 g -> forall n, P n f -> P n g) -> forall (m : Z), P m (fun x => powerRZ x m).
proof: Proof. move => H0 Hpos Hneg Hext m. case: m => [|p|p]. - by rewrite /=. - rewrite -positive_nat_Z. apply: Hext. move => x. by rewrite -pow_powerRZ. exact: Hpos. - rewrite /powerRZ. apply: Hext. move => x. by []. rewrite -Pos2Z.opp_pos. rewrite -positive_nat_Z. exact: Hneg. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval