proposition: Lemma continuous_fst {U V : UniformSpace} (x : U) (y : V) : continuous (fst (B:=V)) (x, y).
proof: Proof. intros P [d Hd]. exists d => z [/= Hz1 Hz2]. by apply Hd => /=. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq