proposition: Fact alpha_2lm_plus_j :〚α (S (2*l*m+j))〛=〚expoZ l (-1)*α (S j)〛.
proof: Proof. generalize (A_plus (2*l*m) j); intros H. apply f_equal with (f := morph22 f) in H. rewrite MU22_morph with (1 := Z2Zp_morph) in H. rewrite A2lm_mod in H. rewrite <- MU22_morph with (1 := Z2Zp_morph) in H. apply M22_proj12 in H. rewrite Z.mul_0_r, Z.mul_0_l, Z.mul_1_r, Z.add_0_l in H. apply H. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)