proposition: Fact all_ones_equation l : 1+(r-1)*∑ l (fun i => power i r) = power l r.
proof: Proof. Proof using Hr. induction l as [ | l IHl ]. * rewrite msum_0, Nat.mul_0_r, power_0; auto. * rewrite msum_plus1; auto. rewrite Nat.mul_add_distr_l, power_S. replace r with (1+(r-1)) at 4 by lia. rewrite Nat.mul_add_distr_r. rewrite <- IHl at 2; ring. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)