proposition: Fact nat_joins_binary_le n m f g : (forall i, i < n -> exists j, j < m /\ f i ≲ g j) -> msum nat_join 0 n f ≲ msum nat_join 0 m g.
proof: Proof. intros H. rewrite nat_joins_binary_le_left. intros i Hi; apply nat_joins_binary_le_right; 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)