proposition: Lemma expo_sufficiency : p = expo r q -> expo_conditions.
proof: Proof. intros H. destruct (le_lt_dec r 0) as [ Hr | Hr ]; red. 1: { left; revert H; replace r with 0 by lia; rewrite mscal_0; tauto. } destruct (eq_nat_dec q 0) as [ Hq | Hq ]. 1: { right; left; subst; rewrite power_of_0; auto. } remember (alpha_nat (q+4) (S r)) as a1. remember (a1+q*q+2) as b. remember (alpha_nat b r) as a2. remember (alpha_nat b (1+r)) as a3. remember (b*q-q*q-1) as m. right; right; split; auto; exists b, m, a1, a2, a3. assert (3 < b) as Hb. { rewrite Heqb. apply Nat.lt_le_trans with (1+(1*1)+2); try lia. repeat apply Nat.add_le_mono; auto. + rewrite Heqa1. apply alpha_nat_mono with (i := 1); lia. + apply Nat.mul_le_mono; lia. } assert (2 <= b) as Hb' by lia. destruct (@alpha_nat_power (q+4)) with (n := r) as (H1 & H2); try lia. assert (q*q+2 <= q*q*q+2*q) as Hq'. { apply H_q3_q; lia. } assert (m <> 0) as Hm. { rewrite Heqm, Heqb. do 2 rewrite Nat.mul_add_distr_r. assert (a1*q <> 0) as Ha1. { intros E; apply Nat.eq_mul_0 in E. destruct E as [ E | ]; try lia. revert E; rewrite Heqa1. apply alpha_nat_gt_0; lia. } revert Ha1; generalize (a1*q); intros x Hx. lia. } assert (expo r q < m) as Hexpo. { rewrite Heqm, Heqb. do 2 rewrite Nat.mul_add_distr_r. rewrite <- Heqa1 in H1. apply Nat.lt_le_trans with (a1*1+1). + rewrite Nat.add_comm, Nat.mul_1_r; apply le_n_S. apply Nat.le_trans with (2 := H1). apply power_mono_r; lia. + rewrite <- Nat.sub_add_distr, <- Nat.add_assoc, <- Nat.add_sub_assoc; try lia. apply Nat.add_le_mono; try lia. apply Nat.mul_le_mono; lia. } repeat (split; auto); try lia. rewrite <- nat2Zp_inj with (Hp := Hm). do 2 rewrite nat2Zp_plus. rewrite Heqa2. revert Hm; rewrite Heqm; intros Hm. rewrite expo_congruence; auto. rewrite <- H, Nat.add_comm, nat2Zp_plus, <- Zp_add_assoc; f_equal. rewrite <- nat2Zp_plus; f_equal. rewrite Heqa3. destruct r as [ | r' ]; try lia. replace (S r' -1) with r' by lia. simpl plus at 2. rewrite alpha_nat_fix_2. generalize (alpha_nat_le Hb' r'); lia. Qed.
imports: Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums) Undecidability.H10.ArithLibs(Zp) Undecidability.H10.Matija(alpha)