proposition: Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0.
proof: Proof. intro; simple induction n; simpl. - intro; red; intro; apply R1_neq_R0; assumption. - intros; red; intro; elim (Rmult_integral x (x ^ n0) H1). + intro; auto. + apply H; assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac