proposition: Fact expand_app p l m : expand p (l++m) = expand p l + power (length l) p * expand p m.
proof: Proof. induction l as [ | x l IH ]; simpl; try lia. rewrite power_S, IH, Nat.mul_add_distr_l, Nat.mul_assoc; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)