proposition: Lemma ex_lim_seq_div (u v : nat -> R) : ex_lim_seq u -> ex_lim_seq v -> Lim_seq v <> 0 -> ex_Rbar_div (Lim_seq u) (Lim_seq v) -> ex_lim_seq (fun n => u n / v n).
proof: Proof. intros. apply Lim_seq_correct in H. apply Lim_seq_correct in H0. exists (Rbar_div (Lim_seq u) (Lim_seq v)). eapply is_lim_seq_div ; try eassumption. by apply Rbar_mult_correct. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy