proposition: Lemma powerRZ_pos_sub (x:R) (n m:positive) : x <> 0 -> x ^Z (Z.pos_sub n m) = x ^ Pos.to_nat n * / x ^ Pos.to_nat m.
proof: Proof. intro Hx. rewrite Z.pos_sub_spec. case Pos.compare_spec; intro H; simpl. - subst; symmetry; auto with real. - rewrite Pos2Nat.inj_sub by trivial. rewrite Pos2Nat.inj_lt in H. rewrite (pow_RN_plus x _ (Pos.to_nat n)) by auto with real. rewrite Nat.sub_add; [ | apply Nat.lt_le_incl; assumption ]. rewrite Rinv_mult, Rinv_inv; auto with real. - rewrite Pos2Nat.inj_sub by trivial. rewrite Pos2Nat.inj_lt in H. rewrite (pow_RN_plus x _ (Pos.to_nat m)) by auto with real. rewrite Nat.sub_add; [ reflexivity | apply Nat.lt_le_incl; assumption ]. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac