proposition: Theorem powerRZ_R1 : forall n : Z, powerRZ 1 n = 1%R.
proof: Proof. intros n; case n; simpl in |- *; auto. intros p; elim (nat_of_P p); simpl in |- *; auto; intros n0 H'; rewrite H'; ring. intros p; elim (nat_of_P p); simpl in |- *. exact Rinv_1. intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H'; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz