proposition: Fact binary_le_sum_powers_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 -> { g | m = sum_powers r n g e /\ forall i, i < n -> g i ≲ f i }.
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 (g & H3 & H4). assert (forall i, i < n -> { h | g i = h * power (e i) r /\ h ≲ f i }) as h_full. { intros i Hi; apply binary_le_power_inv; auto. } set (h := fun i => match le_lt_dec n i with left _ => 0 | right H => proj1_sig (h_full _ H) end). assert (Hh : forall i, i < n -> g i = h i * power (e i) r /\ h i ≲ f i). { intros i Hi; unfold h; destruct (le_lt_dec n i) as [ | H' ]; try lia. apply (proj2_sig (h_full _ H')). } generalize h Hh; clear h_full h Hh; intros h Hh. exists h; split; auto. + rewrite H3. rewrite sum_powers_ortho; auto. * apply msum_ext; intros; apply Hh; auto. * intros i Hi; apply Nat.le_lt_trans with (2 := H1 _ Hi), binary_le_le, Hh; auto. + intros; apply Hh; 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)