proposition: Fact nat_meet_joins_distr_l m n f : m ⇣ msum nat_join 0 n f = msum nat_join 0 n (fun i => m ⇣ f i).
proof: Proof. revert m f; induction n as [ | n IHn ]; intros m f. + do 2 rewrite msum_0; auto. + do 2 rewrite msum_S. rewrite nat_meet_join_distr_l, IHn; auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)