proposition: Lemma Cpow_inv (c:C) n : c<>0 -> (/c)^n = /(c^n).
proof: Proof. intros Hc. induction n; simpl; auto. - symmetry. rewrite <-(Cmult_1_l (/1)). apply Cinv_r, C1_nz. - rewrite IHn. field. auto using Cpow_nz. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy