proposition: Lemma div_absexp_compat : forall (b : Z) (d : nat), Divides d (Z.abs_nat b) -> forall n : nat, Divides d (Z.abs_nat (Exp b (S n))).
proof: Proof. intros b d H. elim H. intros k Hk. simple induction n. split with k. rewrite <- Hk. simpl in |- *. rewrite abs_mult. rewrite mult_comm. simpl in |- *. rewrite <- plus_n_O. reflexivity. intros m IH. replace (Exp b (S (S m))) with (b * Exp b (S m))%Z. rewrite abs_mult. apply div_mult_compat_l. assumption. simpl in |- *. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp