fact: Definition newton_sum n a b : X := CRsum (fun k => (Nbinomial n k) ** (a ^^ k) * (b ^^ (n - k))) n.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid