proposition: Theorem power_div_mult_prime : forall p q r : nat, 0 < q -> 0 < r -> prime p -> power_div (q * r) p = power_div q p + power_div r p.
proof: Proof. intros p q r Hq Hr H; cut (1 < p); [ intros Hp | apply lt_prime; auto ]. apply sym_equal; apply power_div_inv; auto with arith. rewrite <- power_mult; apply divides_mult. apply power_div_divides; auto with arith. apply power_div_divides; auto with arith. red in |- *; intros (q1, H0); case (L_Euclides2 p (div q (power p (power_div q p))) (div r (power p (power_div r p)))); auto. exists q1. apply eq_mult with (power p (power_div q p + power_div r p)). apply Nat.neq_0_lt_0. rewrite <- power_mult; apply lt_O_mult; auto with arith. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. replace (power p (power_div q p + power_div r p) * (q1 * p)) with (q * r). rewrite <- power_mult; auto with arith. apply sym_equal; pattern q at 1 in |- *; rewrite (divides_div (power p (power_div q p)) q); auto with arith. pattern r at 1 in |- *; rewrite (divides_div (power p (power_div r p)) r). ring. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. apply power_div_divides; auto with arith. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. apply power_div_divides; auto with arith. rewrite H0; simpl in |- *; ring. intros (q2, H2); case (power_div_not_divides q p); auto with arith. exists q2. pattern q at 1 in |- *; rewrite (divides_div (power p (power_div q p)) q); auto with arith. rewrite H2; simpl in |- *; ring. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. apply power_div_divides; auto with arith. intros (q2, H2); case (power_div_not_divides r p); auto with arith. exists q2. pattern r at 1 in |- *; rewrite (divides_div (power p (power_div r p)) r); auto with arith. rewrite H2; simpl in |- *; ring. apply power_lt_O; apply Nat.lt_trans with 1; auto with arith. apply power_div_divides; auto with arith. Qed.
imports: Coq(ArithRing)