proposition: Lemma mod_repr_non_0 : forall (n : nat) (x : Z), (0 < x < Z_of_nat n)%Z -> ~ Mod x 0 n.
proof: Proof. intros. intro. elim H. intros. elim (moddivmin x 0 n). rewrite <- Zminus_0_l_reverse. intros. elim (le_not_lt n (Z.abs_nat x)). apply div_le. change (Z.abs_nat 0 < Z.abs_nat x) in |- *. apply ltzlt. unfold Z.le in |- *. simpl in |- *. discriminate. apply Zlt_le_weak. assumption. assumption. apply H3. assumption. rewrite <- (abs_inj n). apply ltzlt. apply Zlt_le_weak. assumption. change (Z_of_nat 0 <= Z_of_nat n)%Z in |- *. apply Znat.inj_le. apply le_O_n. assumption. Qed.
imports: ZArith lemmas natZ exp divides