proposition: Theorem fold_γ_sum : ∀ b n f L, let qr := Q_ring in Σ (i = 0, n), nth_γ (b + i) f L = γ_sum b n f L.
proof: Proof. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM