How to use induction without Fixpoint definition in Coq?
You have an equational specification of the power function. You can prove that it's equivalent to some recursively defined function, in that it has the same values whenever the two functions are passed equal arguments. This is called extensional equality of the two functions.

There is a Zpower function in the standard library, defined recursively:

Fixpoint iter_pos (n:positive) (A:Type) (f:A -&gt; A) (x:A) {struct n} : A :=
  match n with
    | xH =&gt; f x
    | xO n' =&gt; iter_pos n' A f (iter_pos n' A f x)
    | xI n' =&gt; f (iter_pos n' A f (iter_pos n' A f x))
  end.
Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z =&gt; z * x) 1.
Definition Zpower (x y:Z) :=
    match y with
      | Zpos p =&gt; Zpower_pos x p
      | Z0 =&gt; 1
      | Zneg p =&gt; 0
    end.


Here's a quick-and-dirty proof that your function is equal to Zpower for nonnegative exponents.

Lemma neq_int_bool : forall x y, eq_int_bool x y = false &lt;-&gt; x &lt;&gt; y.
Proof.
  intros.
  pose (A := eq_int_bool_axiom x y); clearbody A.
  split; intros.
  intro E; apply &lt;- A in E. assert (false = true); solve [eauto with bool].
  case_eq (eq_int_bool x y); intro E.
  apply -&gt; A in E. elimtype False. solve [auto with bool].
  reflexivity.
Qed.

Lemma pow_x_0 : forall b, pow b 0 = 1.
Proof.
  intros; rewrite _jc_axiom_sum.
  replace (eq_int_bool 0 0) with true. reflexivity.
  symmetry. apply &lt;- eq_int_bool_axiom. reflexivity.
Qed.

Lemma pow_nat_is_power :
  forall b n, pow b (Z_of_nat n) = Zpower b (Z_of_nat n).
Proof.
  induction n; simpl.
  apply pow_x_0.
  rewrite _jc_axiom_sum.
  replace (eq_int_bool (Zpos (P_of_succ_nat n)) 0) with false.
  replace (Zpos (P_of_succ_nat n) - 1) with (Z_of_nat n).
  rewrite IHn; clear IHn.
  rewrite Zpower_pos_nat. rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
  replace (S n) with (1 + n)%nat. 2: solve [auto with arith].
  rewrite Zpower_nat_is_exp.
  unfold Zpower_nat at 1; simpl.
  replace (b * 1) with b. 2: solve [auto with zarith]. f_equal.
  destruct n; simpl.
  reflexivity.
  rewrite Zpower_pos_nat. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. reflexivity.
  rewrite Zpos_P_of_succ_nat. solve [auto with zarith].
  symmetry. apply &lt;- neq_int_bool. intro; discriminate.
Qed.


What about negative exponents? Your function is underspecified; you may want to try to coerce a more precise specification out of Jessie. One possibility is that pow b e = 0 whenever e &lt; 0, which would make pow extensionally equal to Zpower. But it's also possible that pow 1 e = 1 whenever e &lt; 0.

You can also prove properties of the function independently of the function's definition. For example, you can use induction on the arguments to prove interesting properties like

Lemma pow_plus :
  forall b n1 n2,
    pow b (Z_of_nat n1 + Z_of_nat n2) =
    pow b (Z_of_nat n1) * pow b (Z_of_nat n2).
Proof.
  induction n2.
  (*same techniques as above*)
Qed.