proposition: Theorem alpha_sufficiency : alpha_conditions -> 3 < b /\ a = alpha_nat b c.
proof: Proof. intros (H41 & H42 & H43 & H44 & H45 & H46 & H47 & H48 & H49 & H50 & H51 & H52 & H53 & H54 & H55). split; auto. destruct Pell_alpha_nat' with (2 := H42) as (k & Hu); try lia. destruct Pell_alpha_nat with (3 := H43) as (m & Hs & Hr); try lia. destruct Pell_alpha_nat' with (2 := H50) as (n & Hx); try lia. destruct (@division_by_even n (S m)) as (l & j & Hlj); try lia. assert (divides (k*u) (S m)) as H60'. { subst u s; apply alpha_nat_divisibility_2; try lia; auto. } assert (divides u (S m)) as H60. { apply divides_trans with (2 := H60'), divides_mult, divides_refl. } assert (v = alpha_nat b (S (S m)) - alpha_nat b m) as H61. { rewrite alpha_nat_fix_2, <- Hs, <- Hr; lia. } assert (rem x v = rem (alpha_nat b n) v) as H62_1. { rewrite Hx; apply alpha_nat_congruence_0; lia. } assert (rem x u = rem n u) as H65. { rewrite Hx, alpha_nat_congruence_0 with (3 := H48); try lia. f_equal; apply alpha_nat_2; auto. } assert (2 <= b) as Hb by lia. generalize (alpha_nat_2lm Hb H61 Hlj); intros H62_2. assert (2*alpha_nat b j < v) as H63. { apply Nat.le_lt_trans with ((b-2)*alpha_nat b (S m)). { apply Nat.mul_le_mono; try lia. red in Hlj; apply alpha_nat_mono; tauto. } apply Nat.add_lt_mono_l with (2*r). rewrite (Nat.add_comm _ v), H46, Hr, Hs. replace b with (2+(b-2)) at 4 by lia. rewrite Nat.mul_add_distr_r. apply Nat.add_lt_le_mono; auto. apply Nat.mul_lt_mono_pos_l; auto. apply alpha_nat_inc; auto. } rewrite Nat.add_comm, <- rem_plus_rem, <- H62_1, <- H53, rem_plus_rem, Nat.add_comm in H62_2. apply rem_eq_diff_eq in H62_2; auto. assert (2*j < u) as H66. { apply Nat.le_lt_trans with (2 := H51), Nat.mul_le_mono; auto. subst; apply alpha_nat_ge_n; auto. } rewrite <- H55 in H65. assert (c = j) as H67. { destruct H60 as (q & Hq). destruct Hlj as (G1 & [ G2 | (G2 & G3) ]). + apply rem_eq_diff_eq with u; auto. left. rewrite H65, rem_erase with (n := 2*l*q) (r := j); auto. rewrite G2, Hq; ring. + apply rem_eq_diff_eq with u; auto. right. rewrite Nat.add_comm, <- rem_plus_rem, H65, rem_plus_rem, G3. apply rem_prop with (2*l*q); try lia. rewrite Hq, Nat.mul_assoc. assert (2*l*q <> 0) as G4. { intros H. apply Nat.eq_mul_0 in H; destruct H as [ H | H ]; try (subst; discriminate). apply Nat.eq_mul_0 in H; destruct H; lia. } assert (1*u <= 2*l*q*u). { apply Nat.mul_le_mono; auto. revert G4; generalize (2*l*q); intros; lia. } rewrite Nat.mul_1_l in H. revert H; generalize (2*l*q*u); intros; lia. } subst; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)