proposition: Lemma zmoda0_exp_compat : forall a n : Z, (n > 0)%Z -> ZMod a 0 n -> forall m : Z, (m > 0)%Z -> ZMod (ZExp a m) 0 n.
proof: Proof. intros. rewrite <- (inj_abs_pos n). apply modzmod. rewrite expzexp. apply moda0_exp_compat. change (Z.abs_nat n > Z.abs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.gt_lt. assumption. apply Zeq_le. reflexivity. assumption. apply zmodmod. assumption. change (Z.abs_nat m > Z.abs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.gt_lt. assumption. apply Zeq_le. reflexivity. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. Qed.
imports: ZArith lemmas natZ exp divides