proposition: Lemma alpha_Z_ml_eq : 〚 alpha_Z b (S m) 〛 = expoZp (l-1) 〚-1〛 ⊗ nat2Zp Hak2 l ⊗〚 alpha_Z b (S k) 〛 ⊗ expoZp (l-1)〚 alpha_Z b k 〛.
proof: Proof. Proof using Hl Hm. generalize A_m_morph22; intros H. unfold morph22, A, B in H. unfold M22scal, PL22, MZp_I in H. apply M22_proj12 in H. unfold plus in H; rewrite H; clear H. rewrite Zp_mul_comm, Zp_mult_zero, Zp_plus_zero. rewrite Z2Zp_one, Zp_mul_comm, Zp_mult_one; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)