proposition: Lemma zexp_nexp : forall (x : R) x_ (n : nat), (x[//]x_) [^^] (n) [=] x[^]n.
proof: Proof. intros. unfold zexp in |- *. simpl in |- *. elim n. simpl in |- *. algebra. intros. simpl in |- *. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. simpl in |- *. algebra. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)