proposition: Lemma powerRZ_ind (P : Z -> R -> R -> Prop) : (forall x, P 0 x 1%R) -> (forall x n, P (Z.of_nat n) x (x ^ n)%R) -> (forall x n, P ((-(Z.of_nat n))%Z) x (Rinv (x ^ n))) -> forall x (m : Z), P m x (powerRZ x m)%R.
proof: Proof. intros ? ? ? x m. destruct (intP m) as [Hm|n Hm|n Hm]. - easy. - now rewrite <- pow_powerRZ. - unfold powerRZ. destruct n as [|n]; [ easy |]. rewrite Nat2Z.inj_succ, <- Zpos_P_of_succ_nat, Pos2Z.opp_pos. now rewrite <- Pos2Z.opp_pos, <- positive_nat_Z. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac