proposition: Fact sum_power_binary_lt_inv p n f e m : 0 < p <= q -> (forall i j, i < j < n -> f i < f j) -> (forall i j, i < j < n -> e i < e j) -> m ≲ (power p 2-1) * ∑ n (fun i => power (f i) r) -> exists a, m = ∑ n (fun i => a i * power (f i) r) /\ forall i, i < n -> a i < power p 2.
proof: Proof. Proof using Hq Hr. intros H1 H2 H3 H4. rewrite <- sum_0n_scal_l in H4. apply binary_le_sum_powers_inv in H4; auto. + destruct H4 as (a & H5 & H6). exists a; split; auto. intros i Hi; apply power_2_minus_1_gt; auto. + intros i Hi. apply Nat.lt_le_trans with (power p 2). - generalize (@power_ge_1 p 2); intros; lia. - rewrite Hr; apply power_mono_l; 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)