proposition: Theorem pow_R1 : forall (r : R) (n : nat), (r ^ n)%R = 1%R -> Rabs r = 1%R \/ n = 0.
proof: Proof. intros r n H'. case (Req_dec (Rabs r) 1); auto; intros H'1. case (Rdichotomy _ _ H'1); intros H'2. generalize H'; case n; auto. intros n0 H'0. cut (r <> 0%R); [ intros Eq1 | idtac ]. 2: contradict H'0; auto with arith. 2: simpl in |- *; rewrite H'0; rewrite Rmult_0_l; auto with real. cut (Rabs r <> 0%R); [ intros Eq2 | apply Rabs_no_R0 ]; auto. absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0)%R; auto. replace (Rabs (/ r) ^ S n0)%R with 1%R. simpl in |- *; apply Rlt_irrefl; auto. rewrite Rabs_Rinv; auto. rewrite <- Rinv_pow; auto. rewrite RPow_abs; auto. rewrite H'0; rewrite Rabs_right; auto with real. apply Rlt_pow; auto with arith. rewrite Rabs_Rinv; auto. apply Rmult_lt_reg_l with (r := Rabs r). case (Rabs_pos r); auto. intros H'3; case Eq2; auto. rewrite Rmult_1_r; rewrite Rinv_r; auto with real. generalize H'; case n; auto. intros n0 H'0. cut (r <> 0%R); [ intros Eq1 | auto with real ]. 2: contradict H'0; simpl in |- *; rewrite H'0; rewrite Rmult_0_l; auto with real. cut (Rabs r <> 0%R); [ intros Eq2 | apply Rabs_no_R0 ]; auto. absurd (Rabs r ^ 0 < Rabs r ^ S n0)%R; auto with real arith. repeat rewrite RPow_abs; rewrite H'0; simpl in |- *; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz