proposition: Lemma filterlim_plus : forall x y : V, filterlim (fun z : V * V => plus (fst z) (snd z)) (filter_prod (locally x) (locally y)) (locally (plus x y)).
proof: Proof. intros x y. apply (filterlim_filter_le_1 (F := filter_prod (locally_norm x) (locally_norm y))). intros P [Q R LQ LR H]. exists Q R. now apply locally_le_locally_norm. now apply locally_le_locally_norm. exact H. apply (filterlim_filter_le_2 (G := locally_norm (plus x y))). apply locally_norm_le_locally. intros P [eps HP]. exists (ball_norm x (pos_div_2 eps)) (ball_norm y (pos_div_2 eps)). by apply locally_norm_ball_norm. by apply locally_norm_ball_norm. intros u v Hu Hv. apply HP. rewrite /ball_norm /= (double_var eps). apply Rle_lt_trans with (2 := Rplus_lt_compat _ _ _ _ Hu Hv). apply Rle_trans with (2 := norm_triangle _ _). apply Req_le, f_equal. rewrite /minus /= opp_plus -2!plus_assoc. apply f_equal. rewrite 2!plus_assoc. apply f_equal2. by apply plus_comm. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub