proposition: Lemma expzexp : forall x a : Z, ZExp a x = Exp a (Z.abs_nat x).
proof: Proof. intros. induction x as [| p| p]. simpl in |- *. reflexivity. simpl in |- *. reflexivity. simpl in |- *. reflexivity. Qed.
imports: ZArith lemmas natZ