proposition: Lemma inv_zexp_odd : forall (x : R) m, Zodd m -> forall x_ x__, ([--]x[//]x__) [^^] (m) [=] [--] (x[//]x_) [^^] (m).
proof: Proof. intros x m H Hx Hneg. replace m with (m - 1 + 1)%Z. astepl (([--]x[//]Hneg) [^^] (m - 1) [*][--]x). astepr ([--] ((x[//]Hx) [^^] (m - 1) [*]x)). rstepr ((x[//]Hx) [^^] (m - 1) [*][--]x). apply mult_wd. apply inv_zexp_even. apply Zodd_Zeven_min1. assumption. simpl in |- *. auto. algebra. change ((m + -1 + 1)%Z = m) in |- *. rewrite <- Zplus_assoc. simpl in |- *. rewrite <- Zplus_0_r_reverse. reflexivity. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)