proposition: Fact sum_powers_binary_le_inv n f e m : (forall i, i < n -> f i < r) -> (forall i j, i < j < n -> e i < e j) -> m ≲ sum_powers r n f e -> { k : nat & { g : nat -> nat & { h | m = sum_powers r k g (fun i => e (h i)) /\ k <= n /\ (forall i, i < k -> g i <> 0 /\ g i ≲ f (h i)) /\ (forall i, i < k -> h i < n) /\ (forall i j, i < j < k -> h i < h j) } } }.
proof: Proof. Proof using Hq Hr. intros H1 H2 H3. generalize (sinc_injective _ H2); intros H0. simpl in H3; rewrite sum_powers_ortho in H3; auto. apply binary_le_joins_inv in H3. destruct H3 as (k & g & h & H4 & H10 & H5 & H6 & H7). generalize (sinc_injective _ H7); intros H8. assert (forall i, { a | i < k -> g i = a * power (e (h i)) r /\ a <> 0 /\ a ≲ f (h i) }) as H. { intros i. destruct (le_lt_dec k i) as [ H | H ]. * exists 0; intros; lia. * destruct (H5 _ H) as (G1 & G2). rewrite Hr, <- power_mult in G2. apply binary_le_mult_power2_inv in G2; auto. destruct G2 as (a & G2 & G3 & G4). rewrite power_mult, <- Hr in G2. exists a; auto. } set (g' := fun i => proj1_sig (H i)). assert (Hg' : forall i, i < k -> g i = g' i * power (e (h i)) r /\ g' i <> 0 /\ g' i ≲ f (h i)). { intro i; apply (proj2_sig (H i)). } generalize g' Hg'; clear H g' Hg'; intros g' Hg'. exists k, g', h; split; [ | split; [ | split ] ]; auto. - rewrite sum_powers_ortho, H4. * apply msum_ext. intros; apply Hg'; auto. * intros i Hi; apply Nat.le_lt_trans with (f (h i)). + apply binary_le_le, Hg'; auto. + apply H1, H6; auto. * intros ? ? ? ? E; apply H0 in E; auto. - intros; apply Hg'; 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)