proposition: Fact expand_0 p l : Forall (eq 0) l -> expand p l = 0.
proof: Proof. induction 1 as [ | x l H1 H2 IH2 ]; simpl; subst; auto. rewrite IH2, Nat.mul_comm; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)