proposition: Lemma mod_0not1 : forall n : nat, n > 1 -> ~ Mod 0 1 n.
proof: Proof. intros. intro. absurd (Divides n 1). intro. elim (le_not_lt n 1). apply div_le1. assumption. assumption. elim (moddivmin 0 1 n). intros. apply H1. assumption. Qed.
imports: ZArith lemmas natZ exp divides