proposition: Lemma serie_minus_decr : forall f : natO -m> Uopp, serie (fun k => f k - f (S k)) == f O - glb f.
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 UMinus_simpl. apply (sigma_minus_decr f); auto. apply Oeq_sym. apply (lub_comp_eq (f:=UMinus (f O)) f). apply (continuous2_app (F:=UMinus)); auto. Qed.
imports: ALEA(Utheory)