proposition: Lemma zmod_repr_non_0 : forall n x : Z, (0 < x < n)%Z -> ~ ZMod x 0 n.
proof: Proof. intros. intro. elim H. intros. elim (mod_repr_non_0 (Z.abs_nat n) x). split. assumption. rewrite inj_abs_pos. assumption. apply Z.le_ge. apply Z.le_trans with x. apply Zlt_le_weak. assumption. apply Zlt_le_weak. assumption. apply zmodmod. assumption. Qed.
imports: ZArith lemmas natZ exp divides