proposition: Lemma one_zexp : forall z, ([1][//]ring_non_triv _) [^^] (z) [=] ([1]:R).
proof: Proof. intro. pattern z in |- *. apply nats_Z_ind. intro. astepl (([1]:R) [^]n). apply one_nexp. intros. astepl ([1][/] ([1][//]ring_non_triv _) [^^] (n) [//] zexp_resp_ap_zero [1] n (ring_non_triv _)). astepr (([1]:R) [/]OneNZ). apply eq_div. astepr (([1]:R) [*][1][^]n). astepr (([1]:R) [*][1]). algebra. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)