proposition: Theorem alpha_necessity : 3 < b /\ a = alpha_nat b c -> exists u t r s v w x y, alpha_conditions a b c u t r s v w x y.
proof: Proof. intros (H1 & H2). assert (2 <= b) as Hb by lia. destruct find_odd_alpha' with (b_nat := b) (u := 1+2*a+2*c) as (k & Hk1 & Hk2); try lia. remember (alpha_nat b k) as u. remember (alpha_nat b (S k)) as t. remember (u*k) as m. destruct m as [ | m ]. { symmetry in Heqm. apply Nat.eq_mul_0 in Heqm. destruct Heqm; subst; try lia. rewrite alpha_nat_fix_0, rem_of_0 in Hk2; discriminate. } remember (alpha_nat b m) as r. remember (alpha_nat b (S m)) as s. assert (s*s+r*r = 1+b*(s*r)) as Hrs. { rewrite Heqr, Heqs; apply alpha_nat_Pell; auto. } assert (k <> 0) as Hk. { intro; subst; discriminate. } assert (divides (u*u) s) as Hus. { rewrite Hequ, Heqs. apply alpha_nat_divisibility_2; auto. rewrite <- Hequ, Heqm, Nat.mul_comm. apply divides_refl. } assert (2*a < b*s - 2*r) as H3. { apply Nat.lt_le_trans with (2*u). { apply Nat.mul_lt_mono_pos_l; lia. } apply Nat.le_trans with (2*(S m)). { apply Nat.mul_le_mono_l; rewrite Heqm. rewrite <- (Nat.mul_1_r u) at 1. apply Nat.mul_le_mono; lia. } apply Nat.le_trans with (2*alpha_nat b (S m)). { apply Nat.mul_le_mono_l. apply Nat.le_trans with (1 := alpha_nat_ge_n Hb _). apply alpha_nat_mono; lia. } apply Nat.le_trans with (4*s - 2*r). { rewrite Heqs, Heqr. generalize (alpha_nat_inc Hb m); intros; lia. } apply Nat.sub_le_mono_r, Nat.mul_le_mono_r; lia. } remember (b*s-2*r) as v. assert (is_gcd u v 1) as Huv. { split; [ | split ]; try apply divides_1. intros d Hd1 Hd2. assert (divides d s) as F1. { apply divides_trans with (2 := Hus). apply divides_trans with (1 := Hd1). apply divides_mult, divides_refl. } assert (divides d (2*r)) as F2. { apply divides_plus_inv with (1 := Hd2). replace (v+2*r) with (b*s) by lia. apply divides_mult; auto. } apply is_rel_prime_div in F2. + apply divides_plus_inv with (b*(s*r)). * do 2 apply divides_mult; auto. * rewrite Nat.add_comm, <- Hrs. apply divides_plus; apply divides_mult; auto. + apply is_gcd_sym, no_common_prime_is_coprime; try discriminate. intros z G0 G1 G2. apply divides_2_inv in G1; destruct G1; subst z. destruct G0; lia. replace (rem u 2) with 0 in Hk2; try discriminate. symmetry; apply divides_rem_eq; try discriminate. apply divides_trans with (1 := G2); auto. } assert (exists w, rem w u = rem 2 u /\ rem w v = rem b v /\ 2 < w) as Hw. { apply CRT; auto; try lia. } destruct Hw as (w & Hw1 & Hw2 & Hw3). remember (alpha_nat w c) as x. remember (alpha_nat w (S c)) as y. exists u, t, r, s, v, w, x, y; repeat (split; auto); try (subst; (apply alpha_nat_Pell || apply alpha_nat_Pell' || apply alpha_nat_inc)); try lia; auto. + rewrite Heqx, alpha_nat_congruence_0 with (3 := Hw2), H2; try lia. + rewrite Heqx; symmetry. rewrite alpha_nat_congruence_0 with (3 := Hw1); try lia. f_equal; apply alpha_nat_2; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)