proposition: Fact binary_le_joins_inv' m n f : m ≲ msum nat_join 0 n f -> { g | m = msum nat_join 0 n g /\ forall i, i < n -> g i ≲ f i }.
proof: Proof. intros H; exists (fun i => m⇣f i); split. 2: intros; auto. apply binary_le_nat_meet in H. rewrite <- H at 1. apply nat_meet_joins_distr_l. 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)