proposition: Fact base_p_spec n : n = expand p (base_p n).
proof: Proof. apply (proj2_sig (base_p_full n)). Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)