proposition: Fact divides_power p a b : a <= b -> divides (power a p) (power b p).
proof: Proof. * induction 1 as [ | b H IH ]. + apply divides_refl. + apply divides_trans with (1 := IH). rewrite power_S; apply divides_mult, divides_refl. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)