proposition: Fact all_ones_2_joins : 2*w = msum nat_join 0 n (fun i => 2*power i r).
proof: Proof. Proof using Hl Hlq Hw. rewrite Hw_1. apply sum_powers_ortho with (q := 4*q); auto; try lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)