proposition: Fact binary_le_sum_powers : sum_powers r n f e ≲ sum_powers r n g e <-> forall i, i < n -> f i ≲ g i.
proof: Proof. Proof using Hf Hg He Hq Hr. rewrite binary_le_nat_meet, meet_sum_powers. split. + intros E i Hi. apply binary_le_nat_meet. apply power_decomp_unique with (5 := E); auto. intros j Hj; apply Nat.le_lt_trans with (2 := Hf Hj). apply binary_le_le; auto. + intros H; apply msum_ext. intros; f_equal; apply binary_le_nat_meet; 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)