proposition: Theorem power_div_fact_prime_div : forall p n r : nat, 0 < n -> n < power p (2 + r) -> prime p -> power_div (factorial n) p = sum_nm 1 r (fun x => div n (power p x)).
proof: Proof. intros p n r Hn Hr Hp. apply trans_equal with (sum_nm 1 n (fun x : nat => div n (power p x))). rewrite sum_nm_ext with (g := fun x : nat => sum_nm 1 (pred n) (fun y => div_dirac y (power p x))). rewrite sum_nm_com with (f := fun x y => div_dirac y (power p x)). rewrite power_div_fact_prime; auto with arith. apply sum_nm_ext. intros x H1; apply div_dirac_power_div; auto with arith. apply lt_prime; auto. red in |- *; intros H2; Contradict H1; auto with arith. apply Nat.lt_nge; apply Nat.succ_lt_mono; rewrite (Nat.lt_succ_pred 0 n); auto with arith. apply Nat.lt_le_trans with (power p n). apply power_id_lt; auto with arith. apply lt_prime; auto. apply divides_le; auto with arith. apply divides_trans with (2 := H2); auto with arith. intros; apply div_dirac_div; auto with arith. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. apply lt_prime; auto. case (Nat.le_gt_cases n r); intros H1. case (proj1 (Nat.lt_eq_cases _ _) H1); clear H1; intros H1. rewrite sum_nm_split with (q := r) (r := n); auto. rewrite sum_nm_ext with (n := 1 + (1 + n)) (g := fun x : nat => 0); auto. rewrite sum_nm_c with (c := 0); ring. intros x H. apply lt_div_O. apply Nat.lt_le_trans with (power p n); auto with arith. apply power_id_lt; auto with arith. apply lt_prime; auto. apply power_le_mono; auto with arith. apply Nat.lt_trans with 1; auto with arith. apply lt_prime; auto. rewrite H1; auto. rewrite sum_nm_split with (q := n) (r := r); auto. rewrite sum_nm_ext with (n := 1 + (1 + r)) (g := fun x : nat => 0); auto. rewrite sum_nm_c with (c := 0); ring. intros x H. apply lt_div_O. apply Nat.lt_le_trans with (1 := Hr); auto with arith. apply power_le_mono; auto with arith. apply Nat.lt_trans with 1; auto with arith. apply lt_prime; auto. Qed.
imports: Coq(ArithRing)