proposition: Lemma primediv1p : forall p n : nat, Prime p -> Divides n p -> n = 1 \/ n = p.
proof: Proof. intros. unfold Prime in H. elim H. intros. apply (H2 n). assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list