fact: Definition seqs_of_ones u u1 := l+1 < q /\ u = ∑ l (fun i => power (power (S i) 2) r) /\ u1 = ∑ l (fun i => power (power (S (S i)) 2) r).
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)