proposition: Fact all_ones_dio l w : w = ∑ l (fun i => power i r) <-> 1+(r-1)*w = power l r.
proof: Proof. Proof using Hr. split. + intros; subst; apply all_ones_equation. + intros H. apply equation_inj with (2 := H). * lia. * apply all_ones_equation. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)