proposition: Lemma inv_zexp_even : forall (x : R) m, Zeven m -> forall x_ x__, ([--]x[//]x__) [^^] (m) [=] (x[//]x_) [^^] (m).
proof: Proof. intros x m H Hx Hneg. pattern m in |- *. rewrite -> Zeven.Zeven_div2. astepl (([--]x[//]Hneg) [^^] (2) [//]zexp_resp_ap_zero [--]x 2 Hneg) [^^] (Z.div2 m). astepl ([--]x[*][--]x[//]mult_resp_ap_zero _ _ _ Hneg Hneg) [^^] (Z.div2 m). astepl (x[*]x[//]mult_resp_ap_zero _ _ _ Hx Hx) [^^] (Z.div2 m). astepl ((x[//]Hx) [^^] (2) [//]zexp_resp_ap_zero x 2 Hx) [^^] (Z.div2 m). algebra. assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)