proposition: Theorem Rinv_powerRZ : forall (e : R) (n : Z), e <> 0%R -> (/ powerRZ e n)%R = powerRZ e (- n).
proof: Proof. intros e n H. apply Rmult_eq_reg_l with (powerRZ e n); auto with real zarith. rewrite Rinv_r; auto with real zarith. rewrite <- powerRZ_add; auto with real zarith. ring_simplify (n + - n)%Z; simpl in |- *; auto. now apply powerRZ_NOR. now apply powerRZ_NOR. Qed.
imports: Reals ZArith List PeanoNat Psatz