proposition: Lemma absmodzmod : forall a b n : Z, Mod a b (Z.abs_nat n) -> ZMod a b n.
proof: Proof. intros. elim H. intros q Hq. elim Zle_or_lt with 0%Z n. intro. split with q. rewrite inj_abs_pos in Hq. assumption. apply Z.le_ge. assumption. intros. split with (- q)%Z. rewrite inj_abs_neg in Hq. rewrite Zmult_comm. rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse in Hq. rewrite Zmult_comm. assumption. assumption. Qed.
imports: ZArith lemmas natZ exp divides