proposition: Theorem div_dirac_div : forall p q : nat, 0 < p -> 0 < q -> div p q = sum_nm 1 (pred p) (fun x => div_dirac x q).
proof: Proof. intros p q H H0; generalize H; clear H. elim p; auto with arith. intros H1; inversion H1. intros n1; case n1. 2: intros n H H1. 2: replace (pred (S (S n))) with (S (pred (S n))); auto with arith. 2: rewrite sum_nm_f. 2: case (divides_dec q (S (S n))); intros H2. 2: rewrite div_divides_S; auto with arith. 2: rewrite H; auto with arith. 2: rewrite div_dirac_prop1; auto with arith. 2: ring. 2: rewrite div_not_divides_S; auto with arith. 2: rewrite H; auto with arith. 2: rewrite div_dirac_prop2; auto with arith. simpl in |- *. generalize H0; case q; simpl in |- *. intros H1; inversion H1. intros n2; case n2. unfold div in |- *; unfold div_dirac in |- *; simpl in |- *; auto. unfold div in |- *; unfold div_dirac in |- *; simpl in |- *; auto. Qed.
imports: Coq(ArithRing) Bertrand(Summation)