proposition: Lemma seqs_of_ones_dio u u1 : seqs_of_ones u u1 <-> l = 0 /\ u = 0 /\ u1 = 0 /\ 2 <= q \/ 0 < l /\ l+1 < q /\ exists u2 w r0 r1 p1 p2, r0 = r /\ r1+1 = r0 /\ p1 = power (1+l) 2 /\ p2 = power p1 r0 /\ 1+r1*w = r0*p2 /\ u*u = u1 + u2 /\ u1 = (u*u) ⇣ w /\ u2 = (u*u) ⇣ (2*w) /\ r0*r0 + u1 = u + p2 /\ divides (r0*r0*r0*r0) u1.
proof: Proof. split. + intros (H2 & H3 & H4). destruct (le_lt_dec l 0) as [ H1 | H1 ]. - assert (l=0) by lia; subst l. rewrite msum_0 in H3, H4; subst; left; lia. - right; split; auto; split; auto. destruct (const1_cn H1 H2 H3 H4) as (w & u2 & E1 & E2 & E3 & E4 & E5 & E6). exists u2, w, r, (r-1), (power (S l) 2), (power (power (S l) 2) r); repeat (split; auto). * generalize (@power_ge_1 (4*q) 2); intros; lia. * revert E5; rewrite power_S, power_1; auto. * revert E6; do 3 rewrite power_S; rewrite power_1. repeat rewrite Nat.mul_assoc; auto. + intros [ (H1 & H2 & H3 & H4) | (H1 & H2 & u2 & w & r0 & r1 & p1 & p2 & ? & H0 & ? & ? & E1 & E2 & E3 & E4 & E5 & E6) ]. - red; subst; do 2 rewrite msum_0; lia. - assert (r1 = r0-1) by lia; clear H0. subst r0 r1 p1 p2; split; auto. apply obtain_u_u1_value with w u2; auto. * rewrite power_S, power_1; auto. * do 3 rewrite power_S; rewrite power_1. repeat rewrite Nat.mul_assoc; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)