proposition: Fact power_expo x y : power x y = y^x.
proof: Proof. induction x as [ | x IHx ]; simpl. + rewrite power_0; auto. + rewrite power_S; f_equal; auto. Qed.
imports: List Arith Undecidability.Shared.Libs(utils_tac utils_list sums rel_iter gcd pos vec) Undecidability.FRACTRAN(FRACTRAN fractran_utils prime_seq) Undecidability.H10.Dio(dio_logic dio_bounded dio_rt_closure dio_single dio_expo)