proposition: Theorem alpha_nat_2lm_plus_j : nat2Zp Hv' (alpha_nat (2*l*m+j)) = nat2Zp Hv' (alpha_nat j) \/ nat2Zp Hv' (alpha_nat (2*l*m+j)) = Zp_opp Hv' (nat2Zp Hv' (alpha_nat j)).
proof: Proof. generalize (alpha_2lm_plus_j). destruct (expoZ_opp1 l) as [ E | E ]; rewrite E; intros H; [ left | right ]. + repeat rewrite alpha_Z_S in H. rewrite Z2Zp_of_nat, Z.mul_1_l, Z2Zp_of_nat in H; auto. + repeat rewrite alpha_Z_S in H. change (-1) with (-(1)) in H. rewrite Z.mul_opp_l, Z.mul_1_l, Z2Zp_opp in H. repeat rewrite Z2Zp_of_nat in H; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)