proposition: Theorem power_div_fact_prime : forall p n : nat, 0 < n -> prime p -> power_div (factorial n) p = sum_nm 1 (pred n) (fun x => power_div x p).
proof: Proof. intros p n; elim n. intros H1; inversion H1. intros n1; case n1. simpl in |- *; auto. intros n2 Rec Hn2 H. replace (factorial (S (S n2))) with (S (S n2) * factorial (S n2)); auto with arith. rewrite power_div_mult_prime; auto with arith. rewrite Rec; auto with arith. replace (pred (S (S n2))) with (S (pred (S n2))); auto with arith. rewrite sum_nm_f; simpl in |- *; ring. Qed.
imports: Coq(ArithRing)