proposition: Fact A_k_morph22 : morph22 (Z2Zp Hak) (A b k) = (〚alpha_Z b (2+k)〛,Zp_zero Hak,Zp_zero Hak,〚-alpha_Z b k〛).
proof: Proof. Proof using Hm. destruct k as [ | k' ]; try lia. unfold A; apply M22_equal; auto; simpl plus; unfold alpha_Z. + rewrite Z2Zp_opp, Z2Zp_pos, Nat2Z.id, nat2Zp_p, Zp_opp_zero; auto. + rewrite Z2Zp_pos, Nat2Z.id, nat2Zp_p; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)