proposition: Fact A2m_mod : 〘A (2*m)〙= ⊟〘MZ_one〙.
proof: Proof. rewrite <- MZ_expo_A, mscal_mult, MZ_expo_A; auto. rewrite mscal_S, mscal_1; auto. rewrite MU22_morph with (1 := Z2Zp_morph). rewrite Am_iAm_mod at 1. do 2 rewrite <- MI22_morph with (1 := Z2Zp_morph). rewrite <- MU22_morph with (1 := Z2Zp_morph). f_equal. rewrite M22_opp_mult_l with (1 := Zring); f_equal. apply iA_A. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)