proposition: Lemma const1_cn : exists w u2, 1+(r-1)*w = power (S (power (S l) 2)) r /\ u*u = u1 + u2 /\ u1 = (u*u) ⇣ w /\ u2 = (u*u) ⇣ (2*w) /\ power 2 r + u1 = u + power (power (S l) 2) r /\ divides (power 4 r) u1.
proof: Proof. Proof using Hu1 Hu Hr'. exists w, u2; repeat (split; auto). Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)