proposition: Lemma zexp_pred_succ : forall a x : Z, ZExp a (x + 1 - 1) = ZExp a x.
proof: Proof. unfold Zminus in |- *. intros. rewrite Zplus_assoc_reverse. rewrite Zplus_opp_r. rewrite <- Zplus_0_r_reverse. reflexivity. Qed.
imports: ZArith lemmas natZ