proposition: Fact meet_sum_powers : (sum_powers r n f e)⇣(sum_powers r n g e) = sum_powers r n (fun i => f i ⇣ g i) e.
proof: Proof. Proof using Hf Hg He Hq Hr. generalize (sinc_injective _ He); intros H0. simpl; do 3 (rewrite sum_powers_ortho; auto). rewrite nat_meet_joins. + apply msum_ext. intros i Hi; rewrite nat_meet_comm. rewrite nat_meet_joins. rewrite msum_only_one with (i := i); auto. * rewrite nat_meet_comm, Hr, <- power_mult. apply nat_meet_mult_power2. * intros j G1 G2; apply nat_meet_powers_neq; auto. + intros i Hi. apply Nat.le_lt_trans with (2 := Hf Hi). apply binary_le_le; 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)