proposition: Theorem power_div_aux_def : forall p q n : nat, 0 < p -> 1 < q -> p < power q n -> divides (power q (power_div_aux p q n)) p /\ ~ divides (power q (1 + power_div_aux p q n)) p.
proof: Proof. intros p q n; generalize p q; clear p q; elim n. intros p q H H0 H1; Contradict H1; auto with arith. intros n1 Rec p q H1 H2 H3. unfold power_div_aux in |- *. generalize (pdiv_def p q); case (pdiv p q); fold power_div_aux in |- *. intros q1 r1; case r1. intros H4; case H4. apply Nat.lt_trans with (2 := H2); auto with arith. rewrite <- plus_n_O; intros H5 H6; rewrite H5. case (Rec q1 q); auto with arith. apply lt_mult_right_anti with q; auto with arith. repeat rewrite (Nat.mul_comm q); simpl in |- *; rewrite <- H5; auto. apply lt_mult_right_anti with q; auto with arith. replace (q * q1) with p; auto with arith. repeat rewrite (Nat.mul_comm q); auto. simpl in |- *; repeat rewrite (Nat.mul_comm q1). intros H7 H8; split. apply divides_mult1; auto. red in |- *; intros H9; case H8; apply divides_mult2 with (2 := H9); auto. intros r2 H4; case H4; simpl in |- *. apply Nat.lt_trans with (2 := H2); auto with arith. intros H5 H6; split. apply SO_divides_all. red in |- *; intros (q2, H7); absurd (S r2 = 0); auto with arith. apply (div_unic_r p q q1 q2); split; auto. apply Nat.lt_trans with (2 := H2); auto with arith. rewrite H7; ring. Qed.
imports: Coq(ArithRing)