proposition: Lemma C_power_theory : @power_theory C 1 Cmult (@eq C) _ N.to_nat Cpow.
proof: Proof. constructor. destruct n. reflexivity. simpl. induction p. - rewrite Pos2Nat.inj_xI. simpl. now rewrite Nat.add_0_r Cpow_add_r IHp. - rewrite Pos2Nat.inj_xO. simpl. now rewrite Nat.add_0_r Cpow_add_r IHp. - simpl. now rewrite Cmult_1_r. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy