proposition: Lemma FSeries_Sum_strext_IR : forall x y Hx Hy, h x Hx [#] h y Hy -> x [#] y.
proof: Proof. unfold h in |- *; clear h; intros x y Hx Hy H0. unfold series_sum in H0. elim (Lim_strext _ _ H0); intros N HN. simpl in HN; unfold seq_part_sum in HN. elim (Sum0_strext _ _ _ _ HN); intros. exact (pfstrx _ _ _ _ _ _ q). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions