proposition: Lemma Cmod_pow (c:C) n : Cmod (c^n) = (Cmod c ^n)%R.
proof: Proof. induction n; simpl; auto. - apply Cmod_1. - now rewrite Cmod_mult IHn. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy