proposition: Lemma binomial_diag : forall n, Binomial.C n n = 1%R.
proof: Proof. intros n. unfold Binomial.C. rewrite Nat.sub_diag. simpl. field. INR_solve; apply fact_neq_0. Qed.
imports: Lia Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_usual_facts Rtactic MyRIneq Cprop_base Csequence Csequence_facts Cpser_def Cpser_base_facts Cpser_facts Cseries Cseries_facts Cdefinitions Canalysis_def