proposition: Lemma serie_minus_incr : forall f :natO-m> U, serie (fun k => f (S k) - f k) == lub f - f O.
proof: Proof. intros; apply Oeq_trans with (lub (UMinus <_> f O @ f)). unfold serie; apply lub_eq_compat. apply fmon_eq_intro; intro n; rewrite fmon_comp_simpl; rewrite fmon_app_simpl. rewrite UMinus_simpl. apply (sigma_minus_incr f); auto. apply Oeq_sym. apply (lub_comp_eq (f:=UMinus <_> f O) f). red; intro; rewrite fmon_app_simpl. apply (continuous2_left (F:=UMinus) h (f O)); auto. Qed.
imports: ALEA(Utheory)