proposition: Fact alpha_2lm_minus_j :〚α (S (2*l*m-j))〛=〚expoZ (S l) (-1)*α (S j)〛.
proof: Proof. Proof using Hl Hj. generalize (A_minus Hj'); 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. unfold plus in H; rewrite H; f_equal. rewrite mscal_S; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)