proposition: Lemma continuity_2d_pt_const : forall x y c, continuity_2d_pt (fun u v => c) x y.
proof: Proof. intros x y c eps; exists eps; rewrite Rminus_eq_0 Rabs_R0. intros; apply cond_pos. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq