proposition: Fact A2lm_mod : 〘A (2*l*m)〙= 〘MZ_scal (mscal Zmult 1 l (-1)) MZ_one〙.
proof: Proof. replace (2*l*m)%nat with (l*(2*m))%nat by ring. rewrite <- MZ_expo_A, mscal_mult, MZ_expo_A; auto. rewrite expo22_morph with (1 := Z2Zp_morph). rewrite A2m_mod. rewrite <- MI22_morph with (1 := Z2Zp_morph). rewrite <- expo22_morph with (1 := Z2Zp_morph). f_equal. rewrite <- M22scal_MI22 with (1 := Zring). change (-(1)) with (-1). rewrite expo22_scal with (1 := Zring); f_equal. rewrite mscal_of_unit; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)