proposition: Lemma zexp_plus1 : forall (x : R) x_ m, (x[//]x_) [^^] (m + 1) [=] (x[//]x_) [^^] (m) [*]x.
proof: Proof. intros x Hx m. pattern m in |- *. apply nats_Z_ind. intro. replace (Z_of_nat n + 1)%Z with (S n:Z). astepl (x[^]S n). astepr (x[^]n[*]x). algebra. rewrite Znat.inj_S. reflexivity. intros. induction n as [| n Hrecn]. simpl in |- *. algebra. replace (- Z_of_nat (S n) + 1)%Z with (- n)%Z. astepl (([1][/] x[//]Hx) [^]n). astepr (([1][/] x[//]Hx) [^]S n[*]x). simpl in |- *. rational. rewrite Znat.inj_S. replace (Z.succ (Z_of_nat n)) with (1 + Z_of_nat n)%Z. rewrite Zopp_plus_distr. rewrite Zplus_comm. unfold Z.opp at 2 in |- *. rewrite Zplus_assoc. reflexivity. unfold Z.succ in |- *. apply Zplus_comm. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)