proposition: Lemma power_nat : forall x n Hx, x[!]nring n[//]Hx [=] x[^]n.
proof: Proof. intros; unfold power in |- *. induction n as [| n Hrecn]. simpl in |- *; astepr (Exp [0]); simpl in |- *; algebra. simpl in |- *. astepr (Exp (nring n[*]Log x Hx) [*]Exp (Log x Hx)). astepr (Exp (nring n[*]Log x Hx[+]Log x Hx)). simpl in |- *; rational. Qed.
imports: CoRN.transc.Exponential