proposition: Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat.
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); [ intros Eq1 | idtac ]. + assert (Eq2: Rabs r <> 0) by (apply Rabs_no_R0; auto). absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0); auto. * replace (Rabs (/ r) ^ S n0) with 1. -- simpl; apply Rlt_irrefl; auto. -- rewrite Rabs_inv, pow_inv. rewrite RPow_abs; auto. rewrite H'0; rewrite Rabs_right; auto with real rorders. * apply Rlt_pow; auto with arith. rewrite Rabs_inv. 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. + red; intro; absurd (r ^ S n0 = 1); auto. simpl; rewrite H; rewrite Rmult_0_l; auto with real. - generalize H'; case n; auto. intros n0 H'0. cut (r <> 0); [ intros Eq1 | auto with real ]. + cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto. absurd (Rabs r ^ 0 < Rabs r ^ S n0); auto with real arith. repeat rewrite RPow_abs; rewrite H'0; simpl; auto with real. + red; intro; absurd (r ^ S n0 = 1); auto. simpl; rewrite H; rewrite Rmult_0_l; auto with real. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac