proposition: Fact binary_power_split i a : { u : nat & { v | a = u⇡(v*power i r) /\ forall k, u⇣(k*power i r) = 0 } }.
proof: Proof. Proof using Hq Hr. destruct (@euclid a (power i r)) as (u & v & H1 & H2). + generalize (@power_ge_1 i r); intros; lia. + exists v, u. assert (forall k, v ⇣ (k*power i r) = 0) as E. { intros k; replace v with (v+0*power i r) by ring. replace (k*power i r) with (0+k*power i r) by ring. rewrite Hr, <- power_mult. rewrite nat_meet_euclid_power_2, nat_meet_0n, nat_meet_n0; auto. rewrite power_mult, <- Hr; auto. } split; auto. rewrite H1, Nat.add_comm, nat_ortho_plus_join; 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)