proposition: Theorem div_dirac_prop2 : forall p q : nat, 0 < q -> ~ divides q p -> div_dirac p q = 0.
proof: Proof. intros p q H H1; unfold div_dirac in |- *; generalize (not_divides_pdiv p q H H1); case (snd (pdiv p q)); auto with arith. intros H2; case H2; auto. Qed.
imports: Coq(ArithRing) Bertrand(Summation)