(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Definition unit  := unit.

Parameter ignore: forall (a:Type), a  -> unit.

Implicit Arguments ignore.

Parameter label_ : Type.

Parameter at1: forall (a:Type), a -> label_  -> a.

Implicit Arguments at1.

Parameter old: forall (a:Type), a  -> a.

Implicit Arguments old.

Parameter power: Z -> Z  -> Z.


Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).

Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
  n) = (x * (power x (n - 1%Z)%Z))%Z).

Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).

Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).

Theorem Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
  ((0%Z <= m)%Z -> ((power x (n * m)%Z) = (power (power x n) m))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x n m Hn Hm.
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
subst n0; rewrite Power_0; ring_simplify (n * 0)%Z.
apply Power_0.
replace (n*n0)%Z with (n*(n0-1)+n)%Z by ring.
rewrite Power_sum; auto with zarith.
rewrite Hind; auto with zarith.
rewrite <- (Power_1 (power x n)) at 2.
rewrite <- Power_sum; auto with zarith.
ring_simplify (n0 - 1 + 1)%Z; auto.
Qed.
(* DO NOT EDIT BELOW *)