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