proposition: Lemma primebprime : forall n : nat, Prime n <-> bPrime n.
proof: Proof. unfold Prime, bPrime in |- *. split. intro. elim H. split. assumption. intros. apply H1. assumption. intro. elim H. split. assumption. intros. apply H1. unfold lt in |- *. apply le_n_S. apply div_le. apply lt_trans with 1. apply lt_O_Sn. assumption. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list