proposition: Lemma ex_lim_seq_mult (u v : nat -> R) : ex_lim_seq u -> ex_lim_seq v -> ex_Rbar_mult (Lim_seq u) (Lim_seq v) -> ex_lim_seq (fun n => u n * v n).
proof: Proof. intros [lu Hu] [lv Hv] H ; exists (Rbar_mult lu lv). eapply is_lim_seq_mult ; try eassumption. rewrite -(is_lim_seq_unique u lu) //. rewrite -(is_lim_seq_unique v lv) //. by apply Rbar_mult_correct. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy