proposition: Fact binary_le_power_inv i a b : a ≲ b * power i r -> { a' | a = a' * power i r /\ a' ≲ b }.
proof: Proof. Proof using Hq Hr. intros H. destruct (binary_power_split i a) as (u & v & H1 & H2). exists (v⇣b). rewrite binary_le_nat_meet in H. rewrite H1 in H at 1. rewrite nat_meet_comm, nat_meet_join_distr_l in H. rewrite (nat_meet_comm _ u), H2, nat_join_0n, nat_meet_comm in H. rewrite Hr, <- power_mult, nat_meet_mult_power2, power_mult, <- Hr in H. split; 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)