proposition: Lemma expo_necessity : expo_conditions -> p = expo r q.
proof: Proof. unfold expo_conditions. intros [ (H1 & H2) | [ (H1 & H2 & H3) | ((H0 & H1) & b & m & a1 & a2 & a3 & (_ & H2) & (H3 & H4) & (H5 & H6) & H7 & H8 & H9 & H10) ] ]. + subst; auto. + subst; rewrite power_of_0; auto. + assert (m = b*q - q*q -1) as Hm1 by lia. assert (m <> 0) as Hm by lia. assert (q*q+2 <= q*q*q+2*q) as Hq'. { apply H_q3_q; lia. } assert (expo r q < m) as Hq. { rewrite Hm1, H7. do 2 rewrite Nat.mul_add_distr_r. apply Nat.lt_le_trans with (a1*1+1). + rewrite Nat.add_comm, Nat.mul_1_r; apply le_n_S. destruct alpha_nat_power with (b_nat := q+4) (n := r) as (G1 & _); try lia. rewrite H2. apply Nat.le_trans with (2 := G1), 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. } rewrite <- (rem_lt Hm H9), <- (rem_lt Hm Hq). revert H10. rewrite Hm1 in Hm |- *. do 2 rewrite <- nat2Zp_inj with (Hp := Hm). do 2 rewrite nat2Zp_plus. rewrite H4, expo_congruence; auto; [ | lia ]. rewrite H6, nat2Zp_plus. destruct r as [ | r' ]; [ lia | ]. replace (S r' -1) with r' by lia. simpl plus. rewrite alpha_nat_fix_2, nat2Zp_minus. 2: apply alpha_nat_le; lia. intros H; rewrite Zp_opp_plus_eq in H. rewrite H. rewrite (Zp_add_comm _ 〚b * _〛 (∸ _)). repeat rewrite <- Zp_add_assoc. rewrite Zp_minus, Zp_plus_zero_r. rewrite Zp_add_comm, <- Zp_add_assoc. rewrite (Zp_add_comm _ (∸ _)), Zp_minus, Zp_plus_zero_r. trivial. Qed.
imports: Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums) Undecidability.H10.ArithLibs(Zp) Undecidability.H10.Matija(alpha)