proposition: Theorem divides_power : forall a b c : nat, a <= b -> divides (power c a) (power c b).
proof: Proof. intros a b c; exists (power c (b - a)). rewrite power_mult. rewrite (Nat.sub_add _ _ H). reflexivity. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)