proposition: Theorem div_dirac_prop1 : forall p q : nat, 0 < q -> divides q p -> div_dirac p q = 1.
proof: Proof. intros p q H H1; unfold div_dirac in |- *; rewrite divides_pdiv; auto. Qed.
imports: Coq(ArithRing) Bertrand(Summation)