proposition: Fact A_m_morph22 : morph22 (Z2Zp Hak2) (A b m) = MZp_scal (expoZp l〚-1〛⊗ expoZp l〚alpha_Z b k〛) MZp_I ⊞ MZp_scal (expoZp (l-1)〚-1〛⊗ nat2Zp Hak2 l ⊗ 〚alpha_Z b (S k)〛⊗ expoZp (l-1)〚alpha_Z b k〛) (morph22 (Z2Zp Hak2) (B b)).
proof: Proof. Proof using Hl Hm. generalize (MA_expo_A_binomial Hb _ _ Hm); intros H. apply f_equal with (f := morph22 (Z2Zp Hak2)) in H. rewrite msum_morph with (m2 := fun u v => u⊞v) (u2 := MZp_Z) in H. 2: simpl; apply M22_equal; apply Z2Zp_zero. 2: intros (((?&?)&?)&?) (((?&?)&?)&?); apply M22_equal; apply Z2Zp_plus. rewrite msum_first_two in H; try lia. 2: apply M22plus_monoid with (1 := Zp_is_ring Hak2). 2: { intros i Hi. rewrite M22scal_morph with (1 := Z2Zp_morph). repeat rewrite Z2Zp_mult. replace i with (2+(i-2))%nat at 3 by lia. rewrite mscal_plus, Z2Zp_mult; auto. rewrite mscal_S, mscal_1; auto. unfold alpha_Z at 1 2. rewrite <- Nat2Z.inj_mul. fold ak2. rewrite (@Z2Zp_pos _ Hak2 (Z.of_nat ak2)); auto. rewrite Nat2Z.id, nat2Zp_p. repeat rewrite Zp_mult_zero. rewrite (Zp_mul_comm _ _ (Zp_zero _)). repeat rewrite Zp_mult_zero. apply M22scal_zero with (1 := Zp_is_ring Hak2). } rewrite H. repeat rewrite M22scal_morph with (1 := Z2Zp_morph). repeat rewrite Z2Zp_mult. rewrite binomial_n1; try lia. rewrite binomial_n0. rewrite Nat.sub_0_r. repeat rewrite mscal_0. repeat rewrite Z2Zp_one. f_equal. + f_equal; auto. 2: apply M22_equal; try rewrite Z2Zp_one; auto; rewrite Z2Zp_zero; auto. rewrite <- mscal_morph with (m1 := Zmult) (u1 := 1). 2: rewrite Z2Zp_one; auto. 2: apply Z2Zp_mult. rewrite <- mscal_morph with (m1 := Zmult) (u1 := 1). 2: rewrite Z2Zp_one; auto. 2: apply Z2Zp_mult. repeat rewrite <- Zp_mul_assoc. repeat rewrite Zp_mult_one; auto. + repeat (rewrite mscal_1; auto). 2: apply M22mult_monoid with (1 := Zring). rewrite <- mscal_morph with (m1 := Zmult) (u1 := 1). 2: rewrite Z2Zp_one; auto. 2: apply Z2Zp_mult. rewrite <- mscal_morph with (m1 := Zmult) (u1 := 1). 2: rewrite Z2Zp_one; auto. 2: apply Z2Zp_mult. do 4 f_equal. rewrite Z2Zp_pos, Nat2Z.id; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)