proposition: Theorem binomial_Newton n a b : a ⊗ b = b ⊗ a -> expo n (a ⊕ b) = ∑ (S n) (fun i => scal (binomial n i) (expo (n - i) a ⊗ expo i b)).
proof: Proof. Proof using All. destruct M_sum as [ S1 S2 S3 ]. destruct M_times as [ T1 T2 T3 ]. intros Hab; induction n as [ | n IHn ]. + rewrite mscal_0, msum_S, msum_0; simpl. rewrite mscal_0, mscal_0, mscal_1; auto. rewrite S2, T1; auto. + rewrite msum_S with (n := S n), binomial_n0, mscal_1; auto. rewrite mscal_0, Nat.sub_0_r; auto. rewrite T2. rewrite msum_ext with (g := fun i => b ⊗ scal (binomial n i) (expo (n-i) a ⊗ expo i b) ⊕ a ⊗ scal (binomial n (S i)) (expo (n-S i) a ⊗ expo (S i) b)). 2: { intros; rewrite binomial_SS, mscal_plus; auto. replace (S n - S i) with (n-i) by lia; f_equal. * rewrite mscal_S. do 3 rewrite scal_times. do 2 rewrite T3; f_equal. apply mscal_comm; auto. * destruct (le_lt_dec n i). + rewrite binomial_gt; try lia. do 2 rewrite mscal_0. rewrite times_zero_r; auto. + replace (n - i) with (S (n - S i)) by lia. rewrite mscal_S. repeat rewrite scal_times. repeat rewrite T3; auto. } rewrite msum_sum; auto. do 2 rewrite sum_0n_distr_l. rewrite <- IHn. rewrite msum_plus1, binomial_gt; auto. rewrite mscal_0, S2. generalize (msum_S sum z n (fun i => scal (binomial n i) (expo (n-i) a ⊗ expo i b))); intros H. rewrite Nat.sub_0_r, binomial_n0, mscal_1, mscal_0, T2 in H; auto. rewrite S3, (sum_comm (expo _ _)), <- S3. rewrite mscal_S with (x :=a), <- distr_l, <- H, <- IHn. rewrite mscal_S, distr_r. apply sum_comm. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)