proposition: Lemma zexp_S1 : forall a n : Z, (0 <= n)%Z -> ZExp a (n + 1) = (a * ZExp a n)%Z.
proof: Proof. intros. rewrite expzexp. rewrite expzexp. rewrite abs_plus_pos. rewrite plus_comm. change (Exp a (S (Z.abs_nat n)) = (a * Exp a (Z.abs_nat n))%Z) in |- *. apply exp_S. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. Qed.
imports: ZArith lemmas natZ