proposition: Lemma lt_prime : forall p : nat, prime p -> 1 < p.
proof: Proof. intros p; case p. intros H1; Contradict H1; auto. intros n; case n; auto with arith. intros H1; Contradict H1; auto. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)