proposition: Theorem power_div_not_divides : forall p q : nat, 0 < p -> 1 < q -> ~ divides (power q (1 + power_div p q)) p.
proof: Proof. intros p q H1 H2; case (power_div_aux_def p q p); auto with arith. apply power_id_lt; auto. Qed.
imports: Coq(ArithRing)