proposition: Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.
proof: Proof. intros n; case n; simpl; auto. - intros p; elim (Pos.to_nat p); simpl; auto; intros n0 H'; rewrite H'; ring. - intros p; elim (Pos.to_nat p); simpl. + exact Rinv_1. + intros n1 H'; rewrite Rinv_mult; try rewrite Rinv_1; try rewrite H'; auto with real. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac