proposition: Theorem div_dirac_power_div : forall p q r : nat, 0 < p -> 1 < q -> ~ divides (power q (2 + r)) p -> power_div p q = sum_nm 1 r (fun x => div_dirac p (power q x)).
proof: Proof. intros p q r H H0 Hr. pose proof (Nat.eq_0_gt_0_cases (power_div p q)) as Hor. apply or_comm in Hor. case Hor; intros H1; clear Hor. case (proj1 (Nat.lt_eq_cases (pred (power_div p q)) r)). apply le_S_n. rewrite (fun x => Nat.lt_succ_pred 0 x); auto with arith. case (Nat.le_gt_cases (power_div p q) (S r)); auto. intros H2; case Hr; apply divides_trans with (b := power q (power_div p q)); auto with arith. apply power_div_divides; auto with arith. intros Hr1. rewrite sum_nm_split with (r := pred (power_div p q)); auto. rewrite sum_nm_ext with (n := 1) (f := fun x : nat => div_dirac p (power q x)) (g := fun x : nat => 1). rewrite sum_nm_ext with (f := fun x : nat => div_dirac p (power q x)) (g := fun x : nat => 0). repeat rewrite sum_nm_c. rewrite <- mult_n_O; rewrite Nat.mul_1_r; rewrite <- plus_n_O; auto with arith. apply eq_sym. apply (Nat.lt_succ_pred 0 (power_div p q)); auto with arith. intros x H2; replace (1 + pred (power_div p q)) with (power_div p q). apply div_dirac_prop2; auto with arith. apply power_lt_O; auto with arith. red in |- *; intros H3; absurd (divides (power q (1 + power_div p q)) p). apply power_div_not_divides; auto with arith. apply divides_trans with (2 := H3). exists (power q x); rewrite power_mult; auto with arith. apply eq_sym. simpl in |- *; apply (Nat.lt_succ_pred 0 (power_div p q)); auto with arith. intros x H2; apply div_dirac_prop1; auto with arith. apply power_lt_O; auto with arith. apply divides_trans with (power q (power_div p q)). exists (power q (power_div p q - (1 + x))); rewrite power_mult; auto with arith. simpl. rewrite Nat.sub_add; auto with arith. rewrite <- (Nat.lt_succ_pred 0); simpl in |- *; auto with arith. apply power_div_divides; auto with arith. intros Hr1; rewrite <- Hr1. rewrite sum_nm_ext with (n := 1) (f := fun x : nat => div_dirac p (power q x)) (g := fun x : nat => 1). repeat rewrite sum_nm_c. apply eq_sym. rewrite <- (Nat.lt_succ_pred 0); auto with arith. intros x H2; apply div_dirac_prop1; auto with arith. apply power_lt_O; auto with arith. apply divides_trans with (power q (power_div p q)). exists (power q (power_div p q - (1 + x))); rewrite power_mult; auto with arith. simpl. rewrite Nat.sub_add; auto with arith. rewrite <- (Nat.lt_succ_pred 0); simpl in |- *; auto with arith. apply power_div_divides; auto with arith. apply eq_sym in H1. rewrite sum_nm_ext with (f := fun x : nat => div_dirac p (power q x)) (g := fun x : nat => 0). repeat rewrite sum_nm_c. rewrite <- H1; ring. intros x H2. apply div_dirac_prop2; auto with arith. apply power_lt_O; auto with arith. red in |- *; intros H3; case (power_div_not_divides p q); auto with arith. rewrite <- H1; apply divides_trans with (2 := H3); auto with arith. Qed.
imports: Coq(ArithRing)