proposition: Lemma pow_inv x n : (/ x)^n = / x^n.
proof: Proof. induction n as [|n IH] ; simpl. - apply eq_sym, Rinv_1. - rewrite Rinv_mult. now apply f_equal. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac