proposition: Lemma zexp_minus : forall (x : R) x_ m n xn_, (x[//]x_) [^^] (m - n) [=] ((x[//]x_) [^^] (m) [/] (x[//]x_) [^^] (n) [//]xn_).
proof: Proof. intros x Hx m n Hexp. replace (m - n)%Z with (m + - n)%Z. astepl ((x[//]Hx) [^^] (m) [*] (x[//]Hx) [^^] (- n)). astepl ((x[//]Hx) [^^] (m) [*] ([1][/] (x[//]Hx) [^^] (n) [//]Hexp)). astepl ((x[//]Hx) [^^] (m) [*][1][/] (x[//]Hx) [^^] (n) [//]Hexp). algebra. reflexivity. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)