proposition: Lemma zmod_0not1 : forall n : Z, (n > 1)%Z -> ~ ZMod 0 1 n.
proof: Proof. intros. intro. elim (mod_0not1 (Z.abs_nat n)). change (Z.abs_nat n > Z.abs_nat 1) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.lt_trans with 1%Z. unfold Z.lt in |- *. simpl in |- *. reflexivity. apply Z.gt_lt. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. assumption. apply zmodmod. assumption. Qed.
imports: ZArith lemmas natZ exp divides