proposition: Lemma alpha_Z_mnlk_eq : 〚 alpha_Z b (1+m) 〛 = 〚 alpha_Z b (1+n) 〛⊗ expo l〚 alpha_Z b (2+k) 〛.
proof: Proof. Proof using Hm. generalize (A_plus_mult Hb _ _ _ Hm); intros H. apply f_equal with (f := morph22 (Z2Zp Hak)) in H. rewrite MU22_morph with (1 := Z2ZP_morph) in H. rewrite expo22_morph with (1 := Z2ZP_morph) in H. rewrite A_k_morph22 in H. rewrite Diag22_expo with (1 := Zp_is_ring Hak) in H. unfold A, morph22 in H. rewrite MU22_Diag22 with (1 := Zp_is_ring Hak) in H. inversion H; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)