proposition: Lemma zmodmod : forall a b n : Z, ZMod a b n -> Mod a b (Z.abs_nat n).
proof: Proof. unfold ZMod, Mod in |- *. intros. elim H. intros. rewrite H0. elim (Zle_or_lt 0 n). intro. rewrite inj_abs_pos. split with x. reflexivity. apply Z.le_ge. assumption. intro. rewrite inj_abs_neg. split with (- x)%Z. rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_r. rewrite Z.opp_involutive. reflexivity. assumption. Qed.
imports: ZArith lemmas natZ exp divides