proposition: Theorem MA_expo_A_binomial m k l : (m = l * k)%nat -> A m = ∑ (S l) (fun i => MZ_scal ( expoZ (l-i) (-1) * Z.of_nat (binomial l i) * expoZ i (α (S k)) * expoZ (l-i) (α k) ) (MZ_expo i B)).
proof: Proof. Proof using Hb_nat. intro; subst m. rewrite <- MZ_expo_A, mscal_mult, MZ_expo_A, A_is_sum; auto. rewrite binomial_Newton with (zero := MZ_zero); auto. 2: apply M22add_comm with (1 := Zring). 2: apply M22plus_cancel with (1 := Zring). 2: apply M22_mult_distr_l with (1 := Zring). 2: apply M22_mult_distr_r with (1 := Zring). 2: apply M22_equal; ring. apply msum_ext; intros i Hi. repeat rewrite expo22_scal with (1 := Zring). rewrite mscal_of_unit; auto. rewrite <- M22scal_MU22_l with (1 := Zring). rewrite <- M22scal_MU22_r with (1 := Zring). rewrite M22mult_one_l with (1 := Zring). rewrite M22scal_mult with (1 := Zring). rewrite mscal_M22scal with (1 := Zring). rewrite M22scal_mult with (1 := Zring). f_equal. rewrite mscal_Zplus. replace (- α k) with ((-1)*α k) by ring. rewrite mscal_sum; auto; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)