proposition: Fact nat_joins_binary_le_right m n f : (exists i, i < n /\ m ≲ f i) -> m ≲ msum nat_join 0 n f.
proof: Proof. intros (i & H1 & H2). apply binary_le_trans with (1 := H2). clear m H2. revert f i H1; induction n as [ | n IHn ]; intros f [ | i ] Hi; try lia; rewrite msum_S; auto. apply binary_le_trans with (2 := nat_join_right _ _). apply (IHn (fun i => f (S i))); lia. 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)