proposition: Fact double_sum_powers_ortho : ∑ n (fun i => sum_powers r i (f i) (e i)) = msum nat_join 0 n (fun i => ⇧ r i (f i) (e i)).
proof: Proof. Proof using Hq Hr Hf He. rewrite nat_ortho_sum_join. + apply msum_ext; intros; apply dsmpo_1; auto. + intros; do 2 (rewrite dsmpo_1; auto). apply nat_ortho_joins. intros; apply nat_meet_powers_neq; auto. intros E; apply He in E; lia. 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)