proposition: Lemma FSum_FSum0 : forall m n (f : nat -> PartIR) x Hx Hx' Hx'', FSum m n f x Hx [=] FSum0 (S n) f x Hx'[-]FSum0 m f x Hx''.
proof: Proof. intros. simpl in |- *; unfold Sum, Sum1 in |- *; simpl in |- *. apply cg_minus_wd; try apply bin_op_wd_unfolded; try apply Sum0_wd; intros; algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality