proposition: Theorem power_div_inv : forall p q r : nat, 0 < p -> 1 < q -> divides (power q r) p -> ~ divides (power q (1 + r)) p -> r = power_div p q.
proof: Proof. intros p q r H H0 H1 H2. case (Nat.le_gt_cases r (power_div p q)); intros H3. case (proj1 (Nat.lt_eq_cases _ _) H3); intros H4; auto. case H2. apply divides_trans with (power q (power_div p q)). exists (power q (power_div p q - (1 + r))). rewrite power_mult. rewrite Nat.sub_add; auto with arith. apply power_div_divides; auto. absurd (divides (power q (1 + power_div p q)) p). apply power_div_not_divides; auto. apply divides_trans with (2 := H1). exists (power q (r - (1 + power_div p q))). rewrite power_mult. rewrite Nat.sub_add; auto with arith. Qed.
imports: Coq(ArithRing)