proposition: Lemma continuity_2d_pt_mult (f g : R -> R -> R) (x y : R) : continuity_2d_pt f x y -> continuity_2d_pt g x y -> continuity_2d_pt (fun u v => f u v * g u v) x y.
proof: Proof. intros Cf Cg. apply continuity_2d_pt_filterlim in Cf. apply continuity_2d_pt_filterlim in Cg. apply continuity_2d_pt_filterlim. eapply filterlim_comp_2. apply Cf. apply Cg. by apply (filterlim_Rbar_mult (f x y) (g x y) (f x y * g x y)). Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq