proposition: Lemma binary_le_mult_power2_inv m x q : m ≲ x * power q 2 -> m <> 0 -> { y | m = y * power q 2 /\ y <> 0 /\ y ≲ x }.
proof: Proof. intros H1 H2. destruct (@euclid m (power q 2)) as (d & r & H3 & H4). + generalize (@power_ge_1 q 2); intros; lia. + apply binary_le_nat_meet in H1. rewrite Nat.add_comm in H3. rewrite H3, <- (Nat.add_0_l (x*_)) in H1. rewrite nat_meet_euclid_power_2 in H1; auto. rewrite nat_meet_n0 in H1. rewrite (Nat.add_comm r), (Nat.add_comm 0) in H1. apply div_rem_uniq in H1; auto. 2: generalize (@power_ge_1 q 2); intros; lia. destruct H1 as (H0 & H1). subst r; simpl in H3. exists d; split; auto. split. - contradict H2; subst; auto. - rewrite <- H0; 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)