proposition: Lemma continuity_2d_pt_opp (f : R -> R -> R) (x y : R) : continuity_2d_pt f x y -> continuity_2d_pt (fun u v => - f u v) x y.
proof: Proof. apply continuity_1d_2d_pt_comp. apply continuity_pt_opp. apply continuity_pt_id. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq