proposition: Lemma inv_zexp_two : forall (x : R) x_ x__, ([--]x[//]x__) [^^] (2) [=] (x[//]x_) [^^] (2).
proof: Proof. intros. apply inv_zexp_even. simpl in |- *. auto. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)