proposition: Theorem Newton : forall n a b, (a + b) ^^ n == newton_sum n a b.
proof: Proof. intros n a b. induction n; [compute; ring | ]. destruct n; [compute; ring | ]. unfold newton_sum. rewrite CRsum_simpl. rewrite <- CRsum_reindex. rewrite <- (CRsum_eq_compat (fun k => (Nbinomial (S n) k ** a ^^ S k * b ^^ (S (S n) - S k)) + (Nbinomial (S n) (S k) ** a ^^ S k * b ^^ (S (S n) - S k)))). rewrite CRsum_add_compat. rewrite CRpow_simpl. rewrite IHn. rewrite ring_distributive_r. unfold newton_sum. do 2 (rewrite (op_comm (O:=mul)); rewrite CRsum_scal_compat). assert (AP:forall a b c d e f, a == e + c -> b == d + f -> a + b == c + (d + (e + f))) by (intros ? ? ? ? ? ? Hi Hj; rewrite Hi; rewrite Hj; ring); apply AP; clear AP. rewrite CRsum_simpl_r. repeat rewrite Nbinomial_diag. repeat rewrite Nat.sub_diag. apply CRadd_eq_compat. apply CRsum_eq_compat_weak. intro. rewrite <- CRmul_scal_compat. apply CRscal_eq_compat. rewrite CRpow_simpl. simpl; ring. simpl; ring. rewrite <- CRsum_reindex. apply CRadd_eq_compat. simpl; repeat rewrite binomial_zero; ring. apply CRsum_eq_compat; intros j Hj. rewrite (Nat.sub_succ_l _ (S n)); [|lia]. simpl. rewrite <- CRmul_scal_compat. apply CRscal_eq_compat. ring. intros j Hj. rewrite <- CRscal_mult_scal_one. rewrite <- (CRscal_mult_scal_one _ (Nbinomial (S n) (S j))). rewrite <- ring_distributive_l. rewrite CRadd_scal_eq_compat. rewrite Nbinomial_pascal; [ | lia]. rewrite CRscal_mult_scal_one. reflexivity. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid