proposition: Lemma derivable_Cpow : forall (n:nat), derivable (fun z => z ^ n).
proof: Proof. intro n ; induction n. simpl ; apply derivable_const. simpl ; apply derivable_mult ; [apply derivable_id | apply IHn]. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv